Re: [PATCH] git-push.txt: document the behavior of --repo

> 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 <git@drmicha.warpmail.net>
> ---
> 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.