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

From: Junio C Hamano <[email-masked]>
Date: Sun, 17 Feb 2013 18:24:51 -0800

"W. Trevor King" <[email-masked]> writes:

> From: "W. Trevor King" <[email-masked]>
>
> This mirrors existing language in the description of 'git fetch'.
>
> Signed-off-by: W. Trevor King <[email-masked]>
> ---

This looks like a good 'maint' material that can be applied straight
away there in preparation for 1.8.1.4 to me; reviewers watching from
the sideline, please stop me if you see issues.

>  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.