explain better how mirroring works

howto/git.md

@@ -242,6 +242,50 @@ Some repositories are mirrored to https://github.com/torproject
 organization and to the https://gitlab.torproject.org/ server, through
 gitlite hooks.
 
+This used to be through a `git push --mirror $REMOTE` command, but now
+we do a `git push --force $REMOTE '+refs/*:refs/*'`, because the
+`--mirror` argument was destroying merge requests on the GitLab
+side. This, for example, is what you get with `--mirror`:
+
+    user@tor-dev:~/src/gitlab.torproject.org/xxx/xxx$ git push --mirror git@gitlab.torproject.org:ahf/test-push-mirror.git --dry-run
+    To gitlab.torproject.org:ahf/test-push-mirror.git
+       dd75357..964d4c0  master -> master
+     - [deleted]         test-branch
+     - [deleted]         refs/merge-requests/1/head
+     - [deleted]         refs/merge-requests/1/merge
+
+This is exactly what we want to avoid: it correctly moves the master
+branch forward, but the mirroring deletes the `refs/merge-requests/*`
+content at the destination.
+
+Instead with just `--force`:
+
+    user@tor-dev:~/src/gitlab.torproject.org/xxx/xxx$ git push --force git@gitlab.torproject.org:ahf/test-push-mirror.git '+refs/*:refs/*' --dry-run
+    To gitlab.torproject.org:ahf/test-push-mirror.git
+       dd75357..964d4c0  master -> master
+
+Here master gets moved forward properly, but we do not delete anything
+at the destination that is unknown at the source.
+
+Adding --prune here would give the same behavior as git push --mirror:
+
+    user@tor-dev:~/src/gitlab.torproject.org/xxx/xxx$ git push --prune --force git@gitlab.torproject.org:ahf/test-push-mirror.git '+refs/*:refs/*' --dry-run
+    To gitlab.torproject.org:ahf/test-push-mirror.git
+       dd75357..964d4c0  master -> master
+     - [deleted]         test-branch
+     - [deleted]         refs/merge-requests/1/head
+     - [deleted]         refs/merge-requests/1/merge
+
+Since we move everything under `refs/*` with the refspec we pass, this should include tags as well as branches.
+
+The only downside of this approach is this: if a person pushes to
+Gitlab a branch that does not not exist on Gitolite, the branch will
+remain on Gitlab until it's manually deleted. That is fine: if the
+branch does exist, it will simply be overwritten next time Gitolite
+pushes to Gitlab.
+
+See also [bug 41](https://gitlab.torproject.org/tpo/tpa/gitlab/-/issues/41#note_2685994) for a larger discussion on this solution.
+
 ## Archiving a repository
 
 To archive a repository, it must first be deactivated by adding a