From dfafe315dc2ced29e4522b5f56dfe0f9594645e6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 27 Jul 2018 14:33:09 +0200
Subject: [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
---
 .github/CODEOWNERS | 1 -
 1 file changed, 1 deletion(-)

(limited to '.github')

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
 
-- 
cgit v1.2.3