From b08a074b6430e1f273d7ea0bd6f14463e32a6135 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 14 May 2018 11:52:51 +0200
Subject: Pick up user overlays when running GitLab CI on PRs.

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

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 189734a0bc..2a14ed352a 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
+    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
+    then
+        export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+    fi
 else
     if [ -n "${TRAVIS}" ];
     then
-- 
cgit v1.2.3