docs: update description for '--mirror' option for 'git push'

From: "Velasco-Hernandez, Gustavo" <[email protected]>

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.

---
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(-)

index d1978650d60..9d543f823de 100644
@@ -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

"Gustavo Velasco-Hernández via GitGitGadget"

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.

From: "Velasco-Hernandez, Gustavo" <[email protected]>

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. The description has been reworded to describe what is removed, updated or added. (Based on Junio feedback)

---
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-v2
Fetch-It-Via: git fetch https://github.com/gitgitgadget/git pr-git-2028/gustavovelascoh/git-push-update-docs-v2
Pull-Request: https://github.com/git/git/pull/2028

Range-diff vs v1:

1: 2be0bf6e73 ! 1: ab077544b6 docs: update description for '--mirror' option for 'git push'
@@ Commit message

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.
+ on the remote end, in which case, are also deleted. The description has
+ been reworded to describe what is removed, updated or added. (Based on
+ Junio feedback)

## Documentation/git-push.adoc ##
@@ Documentation/git-push.adoc: 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
+ Instead of naming each ref to push, specifies that all
+ refs under refs/ (which includes but is not
+ limited to refs/heads/, refs/remotes/, and refs/tags/)
+- 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.
++ 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 if
++ the configuration option remote.<remote>.mirror is set.

-n::
--dry-run::

 Documentation/git-push.adoc | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

index 5f5408e2c0..77ce4a27c8 100644
@@ -163,12 +163,11 @@ already exists on the remote side.
 	Instead of naming each ref to push, specifies that all
 	refs under `refs/` (which includes but is not
 	limited to `refs/heads/`, `refs/remotes/`, and `refs/tags/`)
-	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.
+	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 if
+	the configuration option `remote.<remote>.mirror` is set.
 
 -n::
 --dry-run::

base-commit: a483264b01b977f3e65a4419103c21e6af7412a2

gitgitgadget

"Gustavo Velasco-Hernández via GitGitGadget"

For this project to use a patch, these two must match.

Please decide, under which name do you want to be known as to this community. Once you decide, please use that chosen name to configure user.name and user.email for the repository you use to work on Git, amend the commit and update the sign-off using the same identity, and the force push to GitGitGadget to /submit (I am not sure about the last two steps as I am not a GGG user)?

Drop "(Based on Junio feedback)" that is not even grammatical ;-) If you want to credit others, it is common to say

    Helped-by: ...

just before your own sign-off. See an example like

https://lore.kernel.org/git/2f78ab2e28c64f05d807cb9460fa62eb1011a57f.1757879060.git.code@khaugsbakk.name/

(by the way, oh, gee, that's an unwieldy long message ID).

It is. Considering I only send out (git send-)emails at most every 15 seconds. ;–(

And I don’t understand why there’s a full SHA1 plus the Unix time.[1] The Unix time ends up being the same on all patches. So you need something more. But the abbreviated SHA1 for each commit guarantees that each Message-ID (msgid) will be unique, no? Why the whole thing?

With an abbreviated SHA1 + Unix time you get:

1. Unique substrings within series from the SHA1s
2. Unique substring among other series from the Unix time unless you generate and send out emails very fast

It wouldn’t surprise me if there are people who have taken advantage of the format to harvest the SHA1 from the message id, even though it isn’t documented (seems like). But I think I’ll be fine with an abbreviated hash in my own tree.

† 1: I did some spelunking and it seems like it has always had this
format.[2] Or at least in the C form. I don’t know if there was a previous shell or Perl form.
† 2: See d1566f7883f (git-format-patch: Make the second and subsequent mails

    replies to the first, 2006-07-14)

KriHau