ci: mirror main and tags to the GitHub mirror #54

Merged

jared merged 1 commits from ci/mirror-to-github into main

2026-08-09 09:04:29 -04:00

Author	SHA1	Message	Date
jared	28c500f47a	ci: mirror main and tags to the GitHub mirror R-CMD-check / check (pull_request) Successful in 3m23s Details R-CMD-check / check (push) Successful in 4m2s Details A plain non-force git push rather than Gitea's built-in push mirror. A push mirror force-updates the refs it owns, so a Merge clicked on a GitHub PR would be silently overwritten on the next sync -- the PR still reading 'Merged' while its commit became unreachable. A non-force push is rejected instead, which turns that into a red CI run. Secret is PAT_GH, not GITHUB_MIRROR_PAT: Gitea reserves the GITHUB_ and GITEA_ prefixes for its own injected variables and refuses secrets using them.	2026-08-08 20:20:56 -04:00

Author

SHA1

Message

Date

jared

28c500f47a

ci: mirror main and tags to the GitHub mirror

R-CMD-check / check (pull_request) Successful in 3m23s

Details

R-CMD-check / check (push) Successful in 4m2s

Details

A plain non-force git push rather than Gitea's built-in push mirror. A
push mirror force-updates the refs it owns, so a Merge clicked on a GitHub
PR would be silently overwritten on the next sync -- the PR still reading
'Merged' while its commit became unreachable. A non-force push is rejected
instead, which turns that into a red CI run.

Secret is PAT_GH, not GITHUB_MIRROR_PAT: Gitea reserves the GITHUB_ and
GITEA_ prefixes for its own injected variables and refuses secrets using
them.

2026-08-08 20:20:56 -04:00