Split the GitHub mirror so Gitea creates its runs and no delete is dropped
Mirror / push (push) Successful in 3s
Test / test (22) (pull_request) Successful in 19s
Test / test (24) (pull_request) Successful in 18s
Test / lint (pull_request) Successful in 24s
Test / test (18) (pull_request) Successful in 18s
Test / test (20) (pull_request) Successful in 17s
Test / test (26) (pull_request) Successful in 25s

This commit is contained in:
2026-09-14 20:38:46 +02:00
parent 84dcf4f3ec
commit 190ddfffa1
4 changed files with 51 additions and 43 deletions
+5
View File
@@ -139,6 +139,11 @@ docker compose run --rm node npm run build
verified rather than asserted.
- `typescript` is pinned to the 6.x line because `typescript-eslint` peer-requires `<6.1.0`. Move to
TypeScript 7 once that constraint lifts.
- GitHub mirrors Gitea through `.gitea/workflows/mirror.yaml`, which never prunes, and
`mirror-delete.yaml`, one run per deleted ref. A delete run that fails or outlives Gitea's queue
timeout leaves the ref on GitHub until it is re-run. Accepted: a stale ref there is harmless, and
refs only GitHub has must survive. Maintainer's call, 2026-09-14; valid while nothing deploys from
GitHub.
## Defects found in 0.4.0