diff options
| author | Maxime Dénès | 2018-11-21 18:33:05 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-21 18:42:12 +0100 |
| commit | fe9340263be1c28fb0dc4c7312cddd72e91253c8 (patch) | |
| tree | 2748374c125599edb8ad76d5125bd23bd51055a0 /dev | |
| parent | 452cb15fd9647dc453cc36614cc469dfa91e3080 (diff) | |
Remove pidetop from CI
pidetop relies on some rather low level API from STM, which we'd like to
change. It does not seem maintained much anymore, and still hasn't moved
to github.
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 19 |
2 files changed, 0 insertions, 26 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 4d5834eeb6..96bc5be7ff 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -215,13 +215,6 @@ : "${fcsl_pcm_CI_ARCHIVEURL:=${fcsl_pcm_CI_GITURL}/archive}" ######################################################################## -# pidetop -######################################################################## -: "${pidetop_CI_REF:=v8.9}" -: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop}" -: "${pidetop_CI_ARCHIVEURL:=${pidetop_CI_GITURL}/get}" - -######################################################################## # ext-lib ######################################################################## : "${ext_lib_CI_REF:=master}" diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh deleted file mode 100755 index 1a9a26843c..0000000000 --- a/dev/ci/ci-pidetop.sh +++ /dev/null @@ -1,19 +0,0 @@ -#!/usr/bin/env bash - -ci_dir="$(dirname "$0")" -. "${ci_dir}/ci-common.sh" - -git_download pidetop - -# 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 - COQLIB="$COQBIN/../lib/coq/" -else - COQLIB="$COQBIN/../" -fi - -( cd "${CI_BUILD_DIR}/pidetop" && dune build -p pidetop @install ) - -echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds |