From 95d977bf0b1825b7d822abbdd062cdb8c38051cb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 22 Jan 2019 23:29:28 +0100
Subject: Remove travis

The azure OSX job replaces the first travis job, and the second always
fails and so is useless.
---
 dev/ci/ci-wrapper.sh | 10 +---------
 1 file changed, 1 insertion(+), 9 deletions(-)

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

diff --git a/dev/ci/ci-wrapper.sh b/dev/ci/ci-wrapper.sh
index 12a70176c2..9ca8f76054 100755
--- a/dev/ci/ci-wrapper.sh
+++ b/dev/ci/ci-wrapper.sh
@@ -6,13 +6,6 @@
 
 set -eo pipefail
 
-function travis_fold {
-    if [ -n "${TRAVIS}" ];
-    then
-	echo "travis_fold:$1:$2"
-    fi
-}
-
 CI_NAME="$1"
 CI_SCRIPT="ci-${CI_NAME}.sh"
 
@@ -22,6 +15,5 @@ cd "${DIR}/../.."
 
 export TIMED=1
 "${DIR}/${CI_SCRIPT}" 2>&1 | tee time-of-build.log
-travis_fold 'start' 'coq.test.timing' && echo 'Aggregating timing log...'
+echo 'Aggregating timing log...'
 python ./tools/make-one-time-file.py time-of-build.log
-travis_fold 'end' 'coq.test.timing'
-- 
cgit v1.2.3