Merge PR #9383: Remove travis

Reviewed-by: Zimmi48
Reviewed-by: vbgl

5 files changed, 5 insertions, 18 deletions

diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 07a13b8204..2e934ff0c0 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -444,9 +444,6 @@ function load_overlay_data {
   else
     export CI_BRANCH=""
     export CI_PULL_REQUEST=""
-    # Used when building 8.8.0 with the latest scripts
-    export TRAVIS_BRANCH=""
-    export TRAVIS_PULL_REQUEST=""
   fi
 
   for overlay in /build/user-overlays/*.sh; do
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 6663fbecf8..10b4f9b044 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -16,14 +16,12 @@ We are currently running tests on the following platforms:
   `./configure`. It should allow complying with this discipline
   without pain.
 
-- Travis CI is used to test the compilation of Coq and run the test-suite on
-  macOS.
-
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
   Windows.
 
 - Azure Pipelines is used to test the compilation of Coq and run the
-  test-suite on Windows. It is expected to replace appveyor eventually.
+  test-suite on Windows and on macOS. It is expected to replace
+  appveyor eventually.
 
 You can anticipate the results of most of these tests prior to submitting your
 PR by running GitLab CI on your private branches. To do so follow these steps:
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'
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 56fdab0c26..5705857d76 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -93,7 +93,7 @@ put the approriate label. Otherwise, they are expected to merge the PR using the
 
 When CI has a few failures which look spurious, restarting the corresponding
 jobs is a good way of ensuring this was indeed the case.
-To restart a job on Travis or on AppVeyor, you should connect using your GitHub
+To restart a job on AppVeyor, you should connect using your GitHub
 account; being part of the Coq organization on GitHub should give you the
 permission to do so.
 To restart a job on GitLab CI, you should sign into GitLab (this can be done
diff --git a/dev/tools/merge-pr.sh b/dev/tools/merge-pr.sh
index a27dacc5a7..72e2930386 100755
--- a/dev/tools/merge-pr.sh
+++ b/dev/tools/merge-pr.sh
@@ -143,7 +143,7 @@ fi
 # Sanity check: PR has an outdated version of CI
 
 BASE_COMMIT=$(echo "$PRDATA" | jq -r '.base.sha')
-CI_FILES=(".travis.yml" ".gitlab-ci.yml" "appveyor.yml")
+CI_FILES=(".gitlab-ci.yml" "appveyor.yml")
 
 if ! git diff --quiet "$BASE_COMMIT" "$LOCAL_BRANCH_COMMIT" -- "${CI_FILES[@]}"
 then