Skip metadata sync successfully when no GitHub mirror exists

Not every Gitea repository has a GitHub push mirror. Zero GitHub mirrors
now ends the run successfully without reading the GitHub secret; several
mirrors still fail. Tests, guides, README, BC-001, PP-001 and MIL-001
are updated to match.

Task: MIL-001#1
Task: MIL-001#5
This commit is contained in:
2026-10-10 07:57:58 +08:00
parent ab122d2073
commit 0c06789a27
9 changed files with 64 additions and 28 deletions
+2 -1
View File
@@ -46,7 +46,8 @@ The workflow runs a preflight and writes nothing to GitHub unless it passes:
1. Both secrets exist and have the expected shape.
2. Gitea accepts the token and the repository is visible with it.
3. Exactly one GitHub push mirror is configured.
3. At most one GitHub push mirror is configured. With none, the run ends
successfully without syncing and the GitHub secret is not read.
4. GitHub accepts the token for the mirror repository **and** the token
reports administration access to it.
+3 -2
View File
@@ -20,9 +20,10 @@ Until delivery is verified, onboard a repository by copying the workflow (below)
1. **Check the prerequisites** in the repository: Actions are enabled, and a
runner with the label `ubuntu-latest` and `python3` is online (see
[Runners](#runners)).
2. **Configure exactly one GitHub push mirror** in the repository settings
2. **Configure one GitHub push mirror** in the repository settings
(Settings, Repository, Mirror settings, Push mirror). The workflow fails
when there are zero or several GitHub mirrors.
when there are several GitHub mirrors. With none, it succeeds without
syncing anything.
3. **Add the two secrets** in the repository (or organization) settings,
using the scopes in [credentials.md](credentials.md):
- `TOKEN_FOR_GITEA`
+6 -2
View File
@@ -29,8 +29,7 @@ never starts, or stops before the step) is a **runner** problem.
| `TOKEN_FOR_GITEA is missing or empty.` | configuration | Add the secret |
| `TOKEN_FOR_GITEA must contain a non-empty GITEA_TOKEN.` | configuration | The JSON form needs a `GITEA_TOKEN` key |
| `Could not determine the Gitea source repository.` | configuration | The run has no repository name; report as a defect |
| `Expected exactly one GitHub push mirror ... found 0` | configuration | Add a GitHub push mirror in the repository settings |
| `Expected exactly one GitHub push mirror ... found N` | configuration | Keep one GitHub push mirror |
| `Expected at most one GitHub push mirror ... found N` | configuration | Keep one GitHub push mirror |
| `Could not determine the GitHub owner and repository ...` | configuration | The mirror address must look like `https://github.com/<owner>/<repo>.git` |
| `Gitea API request failed with HTTP 401` | credentials | Create a new Gitea token and update `TOKEN_FOR_GITEA` |
| `GitHub API request failed with HTTP 401` | credentials | Create a new GitHub token and update `CREDENTIALS_FOR_GITHUB` |
@@ -43,6 +42,11 @@ never starts, or stops before the step) is a **runner** problem.
## Not an error
`No GitHub push mirror configured for <repo>; nothing to sync.` The run
succeeds. Not every Gitea repository has a GitHub mirror, so this is expected
for those. If the repository should have one, add it in the repository
settings.
`WARNING: Gitea returned an invalid push mirror list; GitHub metadata was not
synced.` The run succeeds but nothing was synced. Check that the Gitea
version supports the push mirror API and re-run.