git-push.txt: document the behavior of --repo
commit57b92a77a0aeff49e82cc0bfd14eac9313683766
authorMichael J Gruber <git@drmicha.warpmail.net>
Tue, 27 Jan 2015 12:35:53 +0000 (27 13:35 +0100)
committerJunio C Hamano <gitster@pobox.com>
Wed, 28 Jan 2015 20:56:06 +0000 (28 12:56 -0800)
treed734438de5c09df6a93ce9fac214e60d56ab2576
parent282616c72d1d08a77ca4fe1186cb708c38408d87
git-push.txt: document the behavior of --repo

As per the code, the --repo <repo> option is equivalent to the
<repo> argument to 'git push', but somehow it was documented as
something that is more than that.  [It exists for historical
reasons, back from the time when options had to come before
arguments.]

Say so. [But not that.]

Signed-off-by: Michael J Gruber <git@drmicha.warpmail.net>
Helped-by: Eric Sunshine <sunshine@sunshineco.com>
Signed-off-by: Junio C Hamano <gitster@pobox.com>
Documentation/git-push.txt