1 files changed, 6 insertions, 6 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 189734a0b..f867fd189 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
@@ -67,11 +71,6 @@ git_checkout()
     echo "${_DEST}: $(git log -1 --format='%s | %H | %cd | %aN')" )
 }
 
-checkout_mathcomp()
-{
-  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${1}"
-}
-
 make()
 {
     # +x: add x only if defined
@@ -89,7 +88,8 @@ install_ssreflect()
 {
   echo 'Installing ssreflect' && echo -en 'travis_fold:start:ssr.install\\r'
 
-  checkout_mathcomp "${mathcomp_CI_DIR}"
+  git_checkout "${mathcomp_CI_BRANCH}" "${mathcomp_CI_GITURL}" "${mathcomp_CI_DIR}"
+
   ( cd "${mathcomp_CI_DIR}/mathcomp" && \
     sed -i.bak '/ssrtest/d'     Make && \
     sed -i.bak '/odd_order/d'   Make && \