Re: [PATCH] git-push.txt: document the behavior of --repo

Hello Junio, Michael -- thanks much for clearing this up for me. Appreciate your time. If the --repo option works just like the repository argument to git push, then I would suggest -- just as Junio has done -- that you deprecate this option. Otherwise, it would confuse users. There is also a

git push --repo option not working as described in git manual.

I am using git 2.2.2 and want to report an issue with git push --repo option. git 2.2.2 manual says that git push --repo=public will push to public only if the current branch does not track a remote branch. See http://git-scm.com/docs/git-push However, I see that git pushes even when the