Skip to content

Commit d5d3c0b

Browse files
authored
Migrate coq/opam to use Inria GitLab instead of GitLab.com. (#324)
Following an issue with having hit our quotas on GitLab.com, and by request of @mattam82 in https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/GitLab.2Ecom.20subscription.20.2F.20compute.20minutes. This PR does the following things: - [x] Set up mirroring. - [x] Modify configuration for synchronizing PRs. We should also: - [x] Create the Inria GitLab repository. - [x] Adjust the GitLab CI configuration to use the shared runners available there. (Done in rocq-prover/opam#3181.) - [x] Add a webhook on the Inria GitLab repository.
2 parents 73f6dce + 9c20d5f commit d5d3c0b

File tree

2 files changed

+5
-4
lines changed

2 files changed

+5
-4
lines changed

coqbot-config.toml

+4-3
Original file line numberDiff line numberDiff line change
@@ -24,9 +24,10 @@ app_id="31373"
2424
gitlab="coq/coq"
2525
gitlab_domain="gitlab.inria.fr"
2626

27-
[mappings.opam-coq-archive]
28-
github="coq/opam-coq-archive"
29-
gitlab="coq/opam-coq-archive"
27+
[mappings.opam]
28+
github="coq/opam"
29+
gitlab="coq/opam"
30+
gitlab_domain="gitlab.inria.fr"
3031

3132
[mappings.math-comp]
3233
github="math-comp/math-comp"

src/bot.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -288,7 +288,7 @@ let callback _conn req body =
288288
branch on GitLab."
289289
owner repo )
290290
()
291-
| "math-comp", ("docker-mathcomp" | "math-comp") ->
291+
| "math-comp", ("docker-mathcomp" | "math-comp") | "coq", "opam" ->
292292
(fun () ->
293293
init_git_bare_repository ~bot_info
294294
>>= fun () ->

0 commit comments

Comments
 (0)