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>
This commit is contained in:
Shawn O. Pearce 2007-01-26 00:49:17 -05:00
parent 86a2af6087
commit b972ea59e4

View File

@ -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
}