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

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

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.

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