Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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 coq/opam#3181.) - [x] Add a webhook on the Inria GitLab repository.
- Loading branch information