diff options
author | Junio C Hamano <gitster@pobox.com> | 2015-02-24 22:10:19 -0800 |
---|---|---|
committer | Junio C Hamano <gitster@pobox.com> | 2015-02-24 22:10:19 -0800 |
commit | 2fc85f05452087298023519cf95e04c9343ec69d (patch) | |
tree | 8c6fa7941365a598ba91d09c8144e8f442cdb289 | |
parent | Merge branch 'bc/http-fallback-to-password-after-krb-fails' into maint (diff) | |
parent | git-push.txt: document the behavior of --repo (diff) | |
download | tgif-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.txt | 18 |
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:: |