Skip to content

Commit

Permalink
[ci] Expose updated OCAMLPATH for CI users.
Browse files Browse the repository at this point in the history
This is needed for CI packages that use `META.coq` such as in
coq#7656 .
  • Loading branch information
ejgallego committed Jun 2, 2018
1 parent 3a36761 commit d19d296
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
2 changes: 2 additions & 0 deletions dev/ci/ci-common.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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]*$ ]]
Expand All @@ -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"
Expand Down
4 changes: 1 addition & 3 deletions dev/ci/ci-pidetop.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit d19d296

Please sign in to comment.