Mirror every branch and tag to GitHub from CI, keeping what only GitHub has #5

Merged

lilleman merged 3 commits from github-mirror into main

2026-09-14 20:56:45 +02:00

Author	SHA1	Message	Date
lilleman	c5adfd8e39	Say what the mirror's concurrency group does, and name every way a stale ref survives Test / lint (pull_request) Successful in 20s Details Test / test (26) (pull_request) Successful in 17s Details Mirror / push (push) Successful in 3s Details Test / test (18) (pull_request) Successful in 18s Details Test / test (20) (pull_request) Successful in 18s Details Test / test (22) (pull_request) Successful in 18s Details Test / test (24) (pull_request) Successful in 17s Details	2026-09-14 20:54:04 +02:00
lilleman	14b114afda	Split the GitHub mirror so Gitea creates its runs and no delete is dropped Test / test (18) (pull_request) Successful in 18s Details Mirror / push (push) Successful in 5s Details Test / lint (pull_request) Successful in 20s Details Test / test (22) (pull_request) Successful in 22s Details Test / test (24) (pull_request) Successful in 17s Details Test / test (26) (pull_request) Successful in 17s Details Test / test (20) (pull_request) Successful in 18s Details	2026-09-14 20:40:38 +02:00
lilleman	27e8f288ec	Mirror every branch and tag to GitHub from CI, keeping what only GitHub has	2026-09-14 20:40:38 +02:00