As per the code, the --repo <repo> option is equivalent to the <repo>
argument to 'git push'. [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 <g...@drmicha.warpmail.net>
---
Thanks for digging up the thread, Junio. I never would have thought that
I had been with the Git community for that long already...

 Documentation/git-push.txt | 18 ++----------------
 1 file changed, 2 insertions(+), 16 deletions(-)

diff --git a/Documentation/git-push.txt b/Documentation/git-push.txt
index ea97576..0ad31c4 100644
--- a/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@ -219,22 +219,8 @@ origin +master` to force a push to the `master` branch). 
See the
 `<refspec>...` section above for details.
 
 --repo=<repository>::
-       This option is only relevant if no <repository> argument is
-       passed in the invocation. In this case, 'git push' derives the
-       remote name from the current branch: If it tracks a remote
-       branch, then that remote repository is pushed to. Otherwise,
-       the name "origin" is used. For this latter case, this option
-       can be used to override the name "origin". In other words,
-       the difference between these two commands
-+
---------------------------
-git push public         #1
-git push --repo=public  #2
---------------------------
-+
-is that #1 always pushes to "public" whereas #2 pushes to "public"
-only if the current branch does not track a remote branch. This is
-useful if you write an alias or script around 'git push'.
+       This option is equivalent to the <repository> argument; the latter
+       wins if both are specified.
 
 -u::
 --set-upstream::
-- 
2.3.0.rc1.222.gae238f2

--
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majord...@vger.kernel.org
More majordomo info at  http://vger.kernel.org/majordomo-info.html

Reply via email to