From fe9340263be1c28fb0dc4c7312cddd72e91253c8 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 21 Nov 2018 18:33:05 +0100
Subject: 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.
---
 dev/ci/ci-basic-overlay.sh | 7 -------
 1 file changed, 7 deletions(-)

(limited to 'dev/ci/ci-basic-overlay.sh')

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
@@ -214,13 +214,6 @@
 : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm}"
 : "${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
 ########################################################################
-- 
cgit v1.2.3