aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-06 14:46:40 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-06 14:56:22 +0200
commitb0cd4a2db46f8051ffdf9001f3f9e894aa0b5b25 (patch)
treef31dca1bcca6b2c9fb3df6a6c1e8dc9f23624d7f
parent87c959542e1bed55b14d371f1be02cd60d89082c (diff)
[ci] Add a default target to `Makefile.ci`
So we avoid problems like the one in #7438.
-rw-r--r--Makefile.ci8
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.ci b/Makefile.ci
index 78fec466c..4d4f1df59 100644
--- a/Makefile.ci
+++ b/Makefile.ci
@@ -37,6 +37,12 @@ CI_TARGETS=ci-bignums \
.PHONY: ci-all $(CI_TARGETS)
+ci-help:
+ echo '*** Coq CI system, please specify a target to build.'
+ false
+
+ci-all: $(CI_TARGETS)
+
ci-color: ci-bignums
ci-math-classes: ci-bignums
@@ -49,8 +55,6 @@ ci-formal-topology: ci-corn
$(CI_TARGETS): ci-%:
+./dev/ci/ci-wrapper.sh $*
-ci-all: $(CI_TARGETS)
-
# For emacs:
# Local Variables:
# mode: makefile