From: "Velasco-Hernandez, Gustavo" <Gustavo.Velasco-Hernandez@xxxxxxxxxx>
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@xxxxxxxxx>
---
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
