Merge PR #9383: Remove travis

Reviewed-by: Zimmi48
Reviewed-by: vbgl

1 files changed, 1 insertions, 9 deletions

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'