Skip to content

Drive push/mirror routing from repo_config - #381

Open
lykimq wants to merge 2 commits into
masterfrom
quyen@generic_pr3
Open

Drive push/mirror routing from repo_config#381
lykimq wants to merge 2 commits into
masterfrom
quyen@generic_pr3

Conversation

@lykimq

@lykimq lykimq commented Aug 5, 2026

Copy link
Copy Markdown
Contributor

Replace hardcoded owner/repo push matching with repo_config lookups.

  • Backport when a GitHub project is configured; mirror when GitLab coords are set
  • Add previously hardcoded mirror repos to coqbot-config.toml
  • Add Alcotest coverage for mirror coords and push no-op cases

@lykimq
lykimq force-pushed the quyen@generic_pr3 branch from 1a75d45 to ecbae25 Compare August 5, 2026 10:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant