Labels don't travel with a mirror push -- mirroring copies files, not
repository settings -- but they matter on the GitHub side anyway, because
GitHub reads the same .github/ISSUE_TEMPLATE/ files and silently drops a
labels: entry naming a label it doesn't have. Until now the only thing
keeping the two sets aligned was remembering to do it by hand, which is
exactly the kind of thing that gets forgotten and then fails invisibly.
Add scripts/sync-labels.py and a workflow that runs it daily, on any change
to the script itself, and on manual dispatch. Gitea stays the source of
truth: labels are managed there and GitHub is made to match.
- **Creates and updates** anything missing or drifted. Colors and
descriptions are normalized before comparison -- Gitea returns colors
bare, GitHub sometimes with a leading '#', and a description may be null
on one side and "" on the other -- so a steady state is a true no-op
rather than a rewrite of all 33 labels every run.
- **Deletes only unused extras.** An extra label on the mirror is removed
only when no issue or PR there carries it; one in use is reported with
its count and left alone. An unattended scheduled job must not be able to
strip a label off somebody's issue.
- **Refuses to run on an empty source**, since treating that as truth would
propose deleting every label on the mirror.
- **--dry-run** prints the plan and changes nothing; **--self-test** checks
the diff logic offline against fixtures, and gates the sync step in CI so
a broken diff can't mutate anything.
Stdlib only, so the CI step installs nothing beyond python3. The job is
gated with the same github.server_url check ci.yml uses -- without it the
mirror would queue this forever against a runner that only exists on Gitea.
Labels are matched by name, so a rename reads as delete-plus-create; the
new name is created and the old is pruned only if unused. The two forges
share no stable label ID, so a rename can't be tracked across them.