From: Junio C Hamano <gitster@pobox.com>
Date: Mon, 26 Jan 2015 16:31:29 GMT
Subject: Re: git push --repo option not working as described in git manual.
Message-ID: <xmqqppa1mrku.fsf@gitster.dls.corp.google.com>
In-Reply-To: <loom.20150126T091917-791@post.gmane.org>

The conclusions from the last time we discussed this [*1*], the last
word was that

	git push $some_opt... --repo=$Repo $more_opt... $args...

is designed to work exactly like

	git push $some_opt... $more_opt... $Repo $args...

and the documentation that says otherwise is incorrect.  It seems
that we never followed up on this after we made that determination,
which is unfortunate.  We should at least correct the documentation.


[Reference]

*1* http://thread.gmane.org/gmane.comp.version-control.git/110827/focus=111715