Re: [PATCH] docs: update description for '--mirror' option for 'git push'

[Junio C Hamano <gitster@pobox.com>]

"Gustavo Velasco-Hernández via GitGitGadget"
<gitgitgadget@gmail.com> writes:

> From: "Velasco-Hernandez, Gustavo" <Gustavo.Velasco-Hernandez@netapp.com>
>
> The current description considers only created, updated or deleted refs
> locally. However it does not address the case where new refs were created
> on the remote end, in which case, are also deleted.

Correct, but "they added, we didn't do anything" is a mere special
case of "what we have and they have do not match" and
indistinguishable from "they updated, we removed" for example.

And there is not much point trying to be exhaustive after saying
"... be mirrored to the remote repository."  If we are to improve
the test, we should think about rewriting the whole sentence
starting from "Newly created ...".  After all, they are giving mere
examples and cannot be exhaustive (think: which one of these existing
examples cover "we created, they created differently---their value
goes away and ours win" case).

    ... be mirrored to the remote repository.  This overwrites the
    refs at the remote by (1) removing what is only at the remote,
    (2) force-updating what both ends of the connection have, and
    (3) adding what only exists locally.  This is the default ...

or something, perhaps?

Thanks.

>
> Signed-off-by: Gustavo Velasco-Hernandez <gustavo.velascoh@gmail.com>
> ---
>     Docs: Update description for '--mirror' option for 'git push'
>
> Published-As: https://github.com/gitgitgadget/git/releases/tag/pr-git-2028%2Fgustavovelascoh%2Fgit-push-update-docs-v1
> Fetch-It-Via: git fetch https://github.com/gitgitgadget/git pr-git-2028/gustavovelascoh/git-push-update-docs-v1
> Pull-Request: https://github.com/git/git/pull/2028
>
>  Documentation/git-push.adoc | 7 ++++---
>  1 file changed, 4 insertions(+), 3 deletions(-)
>
> diff --git a/Documentation/git-push.adoc b/Documentation/git-push.adoc
> index d1978650d60..9d543f823de 100644
> --- a/Documentation/git-push.adoc
> +++ b/Documentation/git-push.adoc
> @@ -166,9 +166,10 @@ already exists on the remote side.
>  	be mirrored to the remote repository.  Newly created local
>  	refs will be pushed to the remote end, locally updated refs
>  	will be force updated on the remote end, and deleted refs
> -	will be removed from the remote end.  This is the default
> -	if the configuration option `remote.<remote>.mirror` is
> -	set.
> +	will be removed from the remote end. Any ref existing
> +	in the remote end, but not locally, will be removed too.
> +	This is the default if the configuration option
> +	`remote.<remote>.mirror` is set.
>  
>  -n::
>  --dry-run::
>
> base-commit: 2c2ba49d55ff26c1082b8137b1ec5eeccb4337d1