summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorLibravatar Junio C Hamano <gitster@pobox.com>2015-02-24 22:10:19 -0800
committerLibravatar Junio C Hamano <gitster@pobox.com>2015-02-24 22:10:19 -0800
commit2fc85f05452087298023519cf95e04c9343ec69d (patch)
tree8c6fa7941365a598ba91d09c8144e8f442cdb289
parentMerge branch 'bc/http-fallback-to-password-after-krb-fails' into maint (diff)
parentgit-push.txt: document the behavior of --repo (diff)
downloadtgif-2fc85f05452087298023519cf95e04c9343ec69d.tar.xz
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
-rw-r--r--Documentation/git-push.txt18
1 files changed, 2 insertions, 16 deletions
diff --git a/Documentation/git-push.txt b/Documentation/git-push.txt
index b17283ab7a..58cc59f20c 100644
--- a/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@ -214,22 +214,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. If both
+ are specified, the command-line argument takes precedence.
-u::
--set-upstream::