aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-02 23:19:31 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-02 23:19:31 +0200
commita2a98a4015311af83edcf8fc87aa30a5318bead8 (patch)
tree3de75a62850565fbd53c67d05d2bf7106a7b7f73
parentfa517c333aaa97a04364a1d41b12783cb66c0165 (diff)
parentac4125093abda3a3204436d688f49eae0e7ab340 (diff)
Merge PR#720: Reformat 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)