summaryrefslogtreecommitdiff
path: root/Makefile.ci
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:28 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:28 -0500
commit1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch)
tree5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /Makefile.ci
parent3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff)
parent9ebf44d84754adc5b64fcf612c6816c02c80462d (diff)
Updated version 8.9.0 from 'upstream/8.9.0'
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 \