From cb121381aea4eff595ee9322fa8dca9959e51a59 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 20 Sep 2017 15:11:08 +0200
Subject: In gitlab set TRAVIS_BRANCH so user overlays will work as expected.

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

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 358f527f9e..1bfdf7dfbe 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -5,6 +5,7 @@ set -xe
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN=`pwd`/_install_ci/bin
+    export TRAVIS_BRANCH="$CI_COMMIT_REF_NAME"
 else
     export COQBIN=`pwd`/bin
 fi
-- 
cgit v1.2.3