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
---
 dev/ci/ci-common.sh | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index a68cd0933e..9259a6e0c8 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -20,10 +20,6 @@ else
     then
         export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
         export CI_BRANCH="$TRAVIS_BRANCH"
-    elif [ -n "${CIRCLECI}" ];
-    then
-        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
-        export CI_BRANCH="$CIRCLE_BRANCH"
     else # assume local
         CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
         export CI_BRANCH
-- 
cgit v1.2.3