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 /dev/ci/ci-common.sh | |
| 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 'dev/ci/ci-common.sh')
| -rw-r--r-- | dev/ci/ci-common.sh | 4 |
1 files changed, 0 insertions, 4 deletions
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 |