Already removed from dev in 1120729; main never got it, so it kept
triggering and failing on every push (MIRROR_TOKEN is expired — see
open issue tracked separately). GitHub stays in sync via manual
'git push github' alongside origin, per repo hygiene notes.
17db7a2703