diff options
| author | Théo Zimmermann | 2018-05-22 10:30:51 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-22 10:30:51 +0200 |
| commit | 61e088161858fa7e6ff494cadd7362b9deccd438 (patch) | |
| tree | a88bf6867103dbf87d701cc2e2205e67b5f4e7d0 /dev/ci/ci-pidetop.sh | |
| parent | d6eb4a26648817f6b034e95c02622cadf0fa65ca (diff) | |
| parent | db1719fbac08b5582fafddd4b76ef92f69cc5bc1 (diff) | |
Merge PR #6859: [stm] Make toplevels standalone executables.
Diffstat (limited to 'dev/ci/ci-pidetop.sh')
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh index d04b9637c0..2ac4d21671 100755 --- a/dev/ci/ci-pidetop.sh +++ b/dev/ci/ci-pidetop.sh @@ -8,6 +8,17 @@ pidetop_CI_DIR="${CI_BUILD_DIR}/pidetop" git_checkout "${pidetop_CI_BRANCH}" "${pidetop_CI_GITURL}" "${pidetop_CI_DIR}" -( cd "${pidetop_CI_DIR}" && coq_makefile -f Make -o Makefile.top && make -f Makefile.top "-j${NJOBS}" && make install-toploop -f Makefile.top ) +# Travis / Gitlab have different filesystem layout due to use of +# `-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 -echo -en '4\nexit' | coqtop -main-channel stdfds -toploop pidetop +( cd "${pidetop_CI_DIR}" && OCAMLPATH="$COQOCAMLLIB" jbuilder build @install ) + +echo -en '4\nexit' | "$pidetop_CI_DIR/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds |