git-gui: Always use -v option to push.
tree0a32195f68608c85c22e7e3dcc22f230fcce82d4
-rw-r--r-- 36 .gitignore
-rwxr-xr-x 745 GIT-VERSION-GEN
-rw-r--r-- 1200 Makefile
-rw-r--r-- 1659 TODO
-rwxr-xr-x 114202 git-gui.sh