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

diff --combined Documentation/git-push.txt
index b17283ab7a1cc73c5ec741e0da1128bea2a57a65,aea848a782ac57c9c3d483932b1879adfb022187..58cc59f20cc5a3338f782e09639b8ae8bdc97ae3
--- 1/Documentation/git-push.txt
--- 2/Documentation/git-push.txt
+++ b/Documentation/git-push.txt
@@@ -10,8 -10,7 +10,8 @@@ SYNOPSI
  --------
  [verse]
  'git push' [--all | --mirror | --tags] [--follow-tags] [-n | --dry-run] [--receive-pack=<git-receive-pack>]
 -         [--repo=<repository>] [-f | --force] [--prune] [-v | --verbose] [-u | --set-upstream]
 +         [--repo=<repository>] [-f | --force] [--prune] [-v | --verbose]
 +         [-u | --set-upstream] [--signed]
           [--force-with-lease[=<refname>[:<expect>]]]
           [--no-verify] [<repository> [<refspec>...]]
  
@@@ -34,7 -33,7 +34,7 @@@ When the command line does not specify 
  arguments or `--all`, `--mirror`, `--tags` options, the command finds
  the default `<refspec>` by consulting `remote.*.push` configuration,
  and if it is not found, honors `push.default` configuration to decide
 -what to push (See gitlink:git-config[1] for the meaning of `push.default`).
 +what to push (See linkgit:git-config[1] for the meaning of `push.default`).
  
  
  OPTIONS[[OPTIONS]]
@@@ -130,12 -129,6 +130,12 @@@ already exists on the remote side
        from the remote but are pointing at commit-ish that are
        reachable from the refs being pushed.
  
 +--signed::
 +      GPG-sign the push request to update refs on the receiving
 +      side, to allow it to be checked by the hooks and/or be
 +      logged.  See linkgit:git-receive-pack[1] for the details
 +      on the receiving end.
 +
  --receive-pack=<git-receive-pack>::
  --exec=<git-receive-pack>::
        Path to the 'git-receive-pack' program on the remote
@@@ -214,22 -207,8 +214,8 @@@ origin +master` to force a push to 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::