1 files changed, 1 insertions, 0 deletions
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 \