From 149b0c422027a31972b62457af1bf97bd016e26c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 27 May 2017 16:00:53 +0200
Subject: Gitlab CI

---
 dev/ci/ci-common.sh | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 2711b7ecaa..f1e1515d41 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,11 +2,18 @@
 
 set -xe
 
+if [ -n "${GITLAB_CI}" ];
+then
+    export COQBIN=`pwd`/install/bin
+else
+    export COQBIN=`pwd`/bin
+fi
+export PATH="$COQBIN:$PATH"
+
 # Coq's tools need an ending slash :S, we should fix them.
-export COQBIN=`pwd`/bin/
-export PATH=`pwd`/bin:$PATH
+export COQBIN="$COQBIN/"
 
-ls `pwd`/bin
+ls "$COQBIN"
 
 # Where we clone and build external developments
 CI_BUILD_DIR=`pwd`/_build_ci
-- 
cgit v1.2.3