From b972ea59e422588963bda7be8e04c59728accadf Mon Sep 17 00:00:00 2001 From: "Shawn O. Pearce" Date: Fri, 26 Jan 2007 00:49:17 -0500 Subject: [PATCH] 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 --- git-gui.sh | 1 + 1 file changed, 1 insertion(+) 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 } -- 2.30.2