Release: mirror deletion behaviour note #12

Merged

hannah-vernon merged 2 commits from dev into main

2026-09-09 16:01:56 -05:00

hannah-vernon commented

2026-09-09 16:01:46 -05:00

Owner

Brings main up to dev. Re-raised because PR #11 reported merged with a merge commit that does not exist, leaving main behind.

Brings `main` up to `dev`. Re-raised because PR #11 reported merged with a merge commit that does not exist, leaving `main` behind.

hannah-vernon added 2 commits

2026-09-09 16:01:47 -05:00

Record that the push mirror does not propagate branch deletions 3f2382d743

Observed twice: a merged branch deleted on Forgejo stays on GitHub, so
after every release it must be deleted on both remotes.

Also records that Forgejo's branch DELETE API reports success and drops
the branch from its listing while leaving the git ref in place, which is
why the mirror kept pushing four already-deleted branches.  git ls-remote
is the authority, not the API listing.

No version bump; this is maintainer guidance, not plugin behaviour.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Merge pull request 'Record that the push mirror does not propagate branch deletions' (#10 ) from docs/mirror-deletion-behaviour into dev 85470189eb