Merge PR #9044: Remove pidetop from CI

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