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

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
 }