From b0cd4a2db46f8051ffdf9001f3f9e894aa0b5b25 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 6 May 2018 14:46:40 +0200 Subject: [ci] Add a default target to `Makefile.ci` So we avoid problems like the one in #7438. --- Makefile.ci | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'Makefile.ci') 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 -- cgit v1.2.3