From 0bf48befc4ce8107666cf902b36c3f5c7abc55f1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 2 May 2018 11:08:26 +0200
Subject: [ci]: add pidetop (fix #7336)

---
 dev/ci/ci-basic-overlay.sh | 6 ++++++
 1 file changed, 6 insertions(+)

(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 5cee72cc73..1ae2ad0acb 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -156,3 +156,9 @@
 ########################################################################
 : "${fcsl_pcm_CI_BRANCH:=master}"
 : "${fcsl_pcm_CI_GITURL:=https://github.com/imdea-software/fcsl-pcm.git}"
+
+########################################################################
+# pidetop
+########################################################################
+: "${pidetop_CI_BRANCH:=v8.9}"
+: "${pidetop_CI_GITURL:=https://bitbucket.org/coqpide/pidetop.git}"
-- 
cgit v1.2.3