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 -------
 dev/tools/sudo-apt-get-update.sh | 4 ----
 2 files changed, 11 deletions(-)
 delete mode 100755 dev/tools/sudo-apt-get-update.sh

(limited to 'dev')

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
diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh
deleted file mode 100755
index f8bf6bed41..0000000000
--- a/dev/tools/sudo-apt-get-update.sh
+++ /dev/null
@@ -1,4 +0,0 @@
-#!/usr/bin/env bash
-
-(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err
-! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $?
-- 
cgit v1.2.3