summaryrefslogtreecommitdiff
path: root/Makefile.ci
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /Makefile.ci
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci2
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 20712b60..e86504b7 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -16,6 +16,7 @@ CI_TARGETS=ci-bedrock2 \
ci-coquelicot \
ci-corn \
ci-cpdt \
+ ci-cross-crypto \
ci-elpi \
ci-ext-lib \
ci-equations \
@@ -32,6 +33,7 @@ CI_TARGETS=ci-bedrock2 \
ci-math-classes \
ci-math-comp \
ci-mtac2 \
+ ci-pidetop \
ci-quickchick \
ci-sf \
ci-simple-io \