aboutsummaryrefslogtreecommitdiff
path: root/Makefile.ci
diff options
context:
space:
mode:
authorJason Gross2019-11-26 15:36:56 -0500
committerJason Gross2019-11-27 13:19:55 -0500
commit5f26ee547a9976d1ccfe7cff22d886f7d7df1eef (patch)
treeea879025978ce6eee936fea3b58fe3b63f27b6dc /Makefile.ci
parent309c7ae0ea95d2ca4ade8a6ba88e92ab9b7c08f0 (diff)
[ci] Split out the dependencies of fiat-crypto
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci6
1 files changed, 6 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci
index e9f7fa2db5..8315c16c64 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -19,6 +19,7 @@ CI_TARGETS= \
ci-coquelicot \
ci-corn \
ci-cross-crypto \
+ ci-coqprime \
ci-elpi \
ci-ext-lib \
ci-equations \
@@ -38,6 +39,7 @@ CI_TARGETS= \
ci-perennial \
ci-quickchick \
ci-relation_algebra \
+ ci-rewriter \
ci-sf \
ci-simple-io \
ci-stdlib2 \
@@ -56,10 +58,14 @@ ci-all: $(CI_TARGETS)
ci-color: ci-bignums
+ci-coqprime: ci-bignums
+
ci-math-classes: ci-bignums
ci-corn: ci-math-classes
+ci-fiat-crypto: ci-bedrock2 ci-coqprime ci-rewriter
+
ci-simple-io: ci-ext-lib
ci-quickchick: ci-ext-lib ci-simple-io