git-gui: Always use -v option to push.

Right now `git-push -v` is actually not that verbose; it merely adds
the URL it is pushing to.  This can be informative if you are pushing
to a configured remote, as you may not actually remember what URL that
remote is connected to.  That detail can be important if the push
fails and you attempt to communicate the errors to a 3rd party to help
you resolve the issue.

Signed-off-by: Shawn O. Pearce <spearce@spearce.org>

diff --git a/git-gui.sh b/git-gui.sh
index c42673c8e3b501e154b4edf9c660ff72f0bcc68e..48e1f821deccbc80d05aeec88ebfe1b5f09cbc14 100755 (executable)
--- a/git-gui.sh
+++ b/git-gui.sh
@@ -1285,6 +1285,7 @@ proc push_to {remote} {
                "push $remote" \
                "Pushing changes to $remote"]
        set cmd [list git push]
+       lappend cmd -v
        lappend cmd $remote
        console_exec $w $cmd
 }