From a270f1fef1476b324844e931cbb8195273e2d0f0 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 26 Dec 2017 12:51:37 +0100
Subject: Fix overlay selection for Circle CI.

---
 dev/ci/ci-common.sh | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 23131c94c6..58c90ff11d 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -5,8 +5,17 @@ set -xe
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN=`pwd`/_install_ci/bin
-    export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
+    export CI_BRANCH="$CI_COMMIT_REF_NAME"
 else
+    if [ -n "${TRAVIS}" ];
+    then
+        export CI_PULL_REQUEST="$TRAVIS_PULL_REQUEST"
+        export CI_BRANCH="$TRAVIS_BRANCH"
+    elif [ -n "${CIRCLECI}" ];
+    then
+        export CI_PULL_REQUEST="$CIRCLE_PR_NUMBER"
+        export CI_BRANCH="$CIRCLE_BRANCH"
+    fi
     export COQBIN=`pwd`/bin
 fi
 export PATH="$COQBIN:$PATH"
-- 
cgit v1.2.3