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>

1 files changed, 1 insertions, 0 deletions

diff --git a/git-gui.sh b/git-gui.sh
index c42673c8e..48e1f821d 100755
--- 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
 }