From 88b434a6c61979e1deb4010ce6669b1a4116240a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 1 Oct 2018 19:26:49 +0200
Subject: [ci] [travis] Remove CI contrib testing from Travis.

This was kept as a fallback for some time, not worth keeping it
anymore as our GitLab setup seems mature and reliable enough.
---
 dev/ci/ci-common.sh | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'dev/ci')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 4acc0e86cf..7a450d0d48 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -16,13 +16,6 @@ then
     then
         export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
     fi
-elif [ -n "${TRAVIS}" ];
-then
-    # Travis build, `-local` passed to `configure`
-    export OCAMLPATH="$PWD:$OCAMLPATH"
-    export COQBIN="$PWD/bin"
-    export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
-    export CI_BRANCH="$TRAVIS_BRANCH"
 elif [ -d "$PWD/_build/install/default/" ];
 then
     # Dune build
-- 
cgit v1.2.3