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-pidetop.sh | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

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

diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
index 2ac4d21671..32cba0808e 100755
--- a/dev/ci/ci-pidetop.sh
+++ b/dev/ci/ci-pidetop.sh
@@ -12,13 +12,11 @@ git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}"
 # `-local`. We need to improve this divergence but if we use Dune this
 # "local" oddity goes away automatically so not bothering...
 if [ -d "$COQBIN/../lib/coq" ]; then
-   COQOCAMLLIB="$COQBIN/../lib/"
    COQLIB="$COQBIN/../lib/coq/"
 else
-   COQOCAMLLIB="$COQBIN/../"
    COQLIB="$COQBIN/../"
 fi
 
-( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install )
+( cd "${pidetop_CI_DIR}" && jbuilder build @install )
 
 echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds
-- 
cgit v1.2.3