From 2d6ebc9d8bffd5910f201af75a0b3e45dd9c8988 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Wed, 15 Mar 2017 13:52:40 +0100
Subject: [travis] Overlay for PR#461: Camlp4 removal.

---
 dev/ci/ci-user-overlay.sh | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 028574743..bb193ebb5 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -20,3 +20,12 @@
 #   the name of the branch from which the PR originated. "" if the
 #   current job is a push build.
 
+echo $TRAVIS_PULL_REQUEST_BRANCH
+echo $TRAVIS_PULL_REQUEST
+echo $TRAVIS_BRANCH
+echo $TRAVIS_COMMIT
+
+if [ $TRAVIS_PULL_REQUEST == "461" ] || [ $TRAVIS_BRANCH == "stm+remove_compat_parsing" ]; then
+    mathcomp_CI_BRANCH=no_camlp4_compat
+    mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git
+fi
-- 
cgit v1.2.3