Merge branch 'mg/push-repo-option-doc' into maint

The "git push" documentation made the "--repo=<there>" option
easily misunderstood.

* mg/push-repo-option-doc:
git-push.txt: document the behavior of --repo

diff --cc Documentation/git-push.txt
Simple merge