End the sync log with Skipped when there is no GitHub mirror

Task: MIL-001#1
2026-10-11 10:42:18 +08:00
parent 532e9663cb
commit aa88ea6f8b
7 changed files with 16 additions and 11 deletions
@@ -22,6 +22,8 @@ Each release lists its changes in these groups, in this order:

 ### Changed

+- Sync GitHub mirror metadata: a repository without a GitHub push mirror still
+  succeeds, and the log now ends with the line `Skipped`.
 - The scoped workflows fetch their scripts at the tag `v1` instead of `main`,
  so a merge to `main` reaches consumers only when it is released.