diff options
| author | Emilio Jesus Gallego Arias | 2018-07-27 14:33:09 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-27 14:33:09 +0200 |
| commit | dfafe315dc2ced29e4522b5f56dfe0f9594645e6 (patch) | |
| tree | 59a4c1604988a5e724c52932c11bed4cc3c1f879 /.github/CODEOWNERS | |
| parent | 05ef2d2234578294cd0be6aace2b4ed4c9815d37 (diff) | |
[ci] Remove CircleCI setup.
GitLab setup is quite stable these days thanks to the work of many
people and `coqbot`. We decided to keep CircleCI support for a while
as a safeguard in case something happened in the migration to GitLab,
but these days we are just wasting resources to them and to us. As I'm
afraid CircleCI won't scale for us, the time to remove it has arrived.
Still, CircleCI had some awesome functionality that GitLab's CI
doesn't offer yet, see the links at:
https://github.com/coq/coq/issues/6919#issuecomment-395885573
- https://gitlab.com/gitlab-org/gitlab-ce/issues/29347
- https://gitlab.com/gitlab-org/gitlab-ce/issues/35222
- https://gitlab.com/gitlab-org/gitlab-ce/issues/41947
- https://gitlab.com/gitlab-org/gitlab-ce/issues/47063
Diffstat (limited to '.github/CODEOWNERS')
| -rw-r--r-- | .github/CODEOWNERS | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 384e46723a..20d49e675f 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -9,7 +9,6 @@ ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers -/.circleci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers |