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
---
 test-suite/Makefile | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/Makefile b/test-suite/Makefile
index 33b4023272..b8aac8b6f8 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -192,10 +192,6 @@ PRINT_LOGS?=
 TRAVIS?= # special because we want to print travis_fold directives
 ifdef APPVEYOR
 PRINT_LOGS:=APPVEYOR
-else
-ifdef CIRCLECI
-PRINT_LOGS:=CIRCLECI
-endif #CIRCLECI
 endif #APPVEYOR
 
 report: summary.log
-- 
cgit v1.2.3