3 files changed, 14 insertions, 3 deletions
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"
diff --git a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
index af4a96f4ae..7716bcb59a 100644
--- a/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
+++ b/dev/ci/user-overlays/00669-maximedenes-ssr-merge.sh
@@ -1,4 +1,4 @@
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index 9146d3d521..9f0377ceea 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -7,8 +7,10 @@ The name of your overlay file should be of the form `five_digit_PR_number-GitHub
 Example: `00669-maximedenes-ssr-merge.sh` containing
 
 ```
-if [ "$TRAVIS_PULL_REQUEST" = "669" ] || [ "$TRAVIS_BRANCH" = "ssr-merge" ]; then
+if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
     mathcomp_CI_BRANCH=ssr-merge
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 ```
+
+(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh))