From d19d296c2b584954e9adb97eed7c705cc1db4bc7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 2 Jun 2018 19:39:28 +0200
Subject: [ci] Expose updated `OCAMLPATH` for CI users.

This is needed for CI packages that use `META.coq` such as in
https://github.com/coq/coq/pull/7656 .
---
 dev/ci/ci-common.sh | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'dev/ci/ci-common.sh')

diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index f867fd189b..5b5cbd11ae 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -8,6 +8,7 @@ export NJOBS
 
 if [ -n "${GITLAB_CI}" ];
 then
+    export OCAMLPATH="$PWD/_install_ci/lib:$OCAMLPATH"
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
     if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
@@ -27,6 +28,7 @@ else
         CI_BRANCH="$(git rev-parse --abbrev-ref HEAD)"
         export CI_BRANCH
     fi
+    export OCAMLPATH="$PWD:$OCAMLPATH"
     export COQBIN="$PWD/bin"
 fi
 export PATH="$COQBIN:$PATH"
-- 
cgit v1.2.3