diff options
| -rw-r--r-- | .gitlab-ci.yml | 3 | ||||
| -rw-r--r-- | Makefile.ci | 1 | ||||
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 7 | ||||
| -rwxr-xr-x | dev/ci/ci-pidetop.sh | 19 |
4 files changed, 0 insertions, 30 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 0ebac839fc..45597851ef 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -436,9 +436,6 @@ ci-mtac2: ci-paramcoq: <<: *ci-template -ci-pidetop: - <<: *ci-template - ci-plugin_tutorial: <<: *ci-template diff --git a/Makefile.ci b/Makefile.ci index 88ea64974a..d0b87fc58b 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,6 @@ CI_TARGETS= \ ci-math-comp \ ci-mtac2 \ ci-paramcoq \ - ci-pidetop \ ci-plugin_tutorial \ ci-quickchick \ ci-sf \ 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 |