1 files changed, 19 insertions, 0 deletions
diff --git a/dev/ci/ci-pidetop.sh b/dev/ci/ci-pidetop.sh
new file mode 100755
index 00000000..d22b9c8f
--- /dev/null
+++ b/dev/ci/ci-pidetop.sh
@@ -0,0 +1,19 @@
+#!/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" && jbuilder build @install )
+
+echo -en '4\nexit' | "${CI_BUILD_DIR}/pidetop/_build/install/default/bin/pidetop" -coqlib "$COQLIB" -main-channel stdfds