aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.ci
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-05-30 22:59:33 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-05-31 16:06:55 -0400
commitac4125093abda3a3204436d688f49eae0e7ab340 (patch)
treeb1eb27504172591651a2658137e71f4870c45a62 /Makefile.ci
parenteed90d1bd867dce59f6bf1b2bf769fff188f128b (diff)
Reformat Makefile.ci
Diffstat (limited to 'Makefile.ci')
-rw-r--r--Makefile.ci25
1 files changed, 21 insertions, 4 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 013685218..e4c63af9d 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -1,7 +1,24 @@
-CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \
- ci-color ci-math-classes ci-tlc ci-fiat-crypto ci-fiat-parsers \
- ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq \
- ci-unimath ci-vst ci-bedrock-src ci-bedrock-facade ci-formal-topology
+CI_TARGETS=ci-all \
+ ci-bedrock-facade \
+ ci-bedrock-src \
+ ci-color \
+ ci-compcert \
+ ci-coquelicot \
+ ci-cpdt \
+ ci-fiat-crypto \
+ ci-fiat-parsers \
+ ci-flocq \
+ ci-formal-topology \
+ ci-geocoq \
+ ci-hott \
+ ci-iris-coq \
+ ci-math-classes \
+ ci-math-comp \
+ ci-metacoq \
+ ci-sf \
+ ci-tlc \
+ ci-unimath \
+ ci-vst
.PHONY: $(CI_TARGETS)