aboutsummaryrefslogtreecommitdiff
path: root/Makefile.ci
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci2
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 677fd734bf..de03ee8e84 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -18,7 +18,6 @@ CI_TARGETS= \
ci-coq_dpdgraph \
ci-coquelicot \
ci-corn \
- ci-cpdt \
ci-cross-crypto \
ci-elpi \
ci-ext-lib \
@@ -41,7 +40,6 @@ CI_TARGETS= \
ci-sf \
ci-simple-io \
ci-stdlib2 \
- ci-tlc \
ci-unimath \
ci-verdi-raft \
ci-vst