diff options
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 15 | ||||
| -rw-r--r-- | dev/ci/user-overlays/06859-ejgallego-stm+top.sh | 6 |
2 files changed, 19 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 diff --git a/dev/ci/user-overlays/06859-ejgallego-stm+top.sh b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh new file mode 100644 index 0000000000..ca0076b468 --- /dev/null +++ b/dev/ci/user-overlays/06859-ejgallego-stm+top.sh @@ -0,0 +1,6 @@ +#!/bin/sh + +if [ "$CI_PULL_REQUEST" = "6859" ] || [ "$CI_BRANCH" = "stm+top" ] || [ "$CI_BRANCH" = "pr-6859" ]; then + pidetop_CI_BRANCH=stm+top + pidetop_CI_GITURL=https://bitbucket.org/ejgallego/pidetop.git +fi |