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

---
 Makefile.ci | 1 +
 1 file changed, 1 insertion(+)

(limited to 'Makefile.ci')

diff --git a/Makefile.ci b/Makefile.ci
index 37b14ed91..78fec466c 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -29,6 +29,7 @@ CI_TARGETS=ci-bignums \
     ci-math-classes \
     ci-math-comp \
     ci-mtac2 \
+    ci-pidetop \
     ci-sf \
     ci-tlc \
     ci-unimath \
-- 
cgit v1.2.3