Re: [PATCH v3 3/9] user-manual: Give 'git push -f' as an alternative to +master

> From: "W. Trevor King" <wking@tremily.us>
>
> This mirrors existing language in the description of 'git fetch'.
>
> Signed-off-by: W. Trevor King <wking@tremily.us>
> ---

>  Documentation/user-manual.txt | 7 +++++++
>  1 file changed, 7 insertions(+)
>
> diff --git a/Documentation/user-manual.txt b/Documentation/user-manual.txt
> index dbffd0a..ba06b7e 100644
> --- a/Documentation/user-manual.txt
> +++ b/Documentation/user-manual.txt
> @@ -2051,6 +2051,13 @@ branch name with a plus sign:
>  $ git push ssh://yourserver.com/~you/proj.git +master
>  -------------------------------------------------
>  
> +Note the addition of the `+` sign.  Alternatively, you can use the
> +`-f` flag to force the remote update, as in:
> +
> +-------------------------------------------------
> +$ git push -f ssh://yourserver.com/~you/proj.git master
> +-------------------------------------------------
> +
>  Normally whenever a branch head in a public repository is modified, it
>  is modified to point to a descendant of the commit that it pointed to
>  before.  By forcing a push in this situation, you break that convention.