aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ci
diff options
context:
space:
mode:
authorGravatar Anton Trunov <anton.a.trunov@gmail.com>2018-04-20 18:28:34 +0200
committerGravatar Anton Trunov <anton.a.trunov@gmail.com>2018-04-20 19:09:34 +0200
commit80b2a82d25fc9117270b9a052e4071d87eb6755f (patch)
tree07f28fa619d21cd5e1d4a640666db0bdf9836782 /Makefile.ci
parent239e28f71192d7537bc6ea283c806ba28fa1c016 (diff)
CI: add fcsl-pcm
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci1
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 3c26bf964..6b30f8723 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -17,6 +17,7 @@ CI_TARGETS=ci-bignums \
ci-cpdt \
ci-elpi \
ci-equations \
+ ci-fcsl-pcm \
ci-fiat-crypto \
ci-fiat-parsers \
ci-flocq \