diff options
| author | Emilio Jesus Gallego Arias | 2018-05-06 14:46:40 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-05-06 14:56:22 +0200 |
| commit | b0cd4a2db46f8051ffdf9001f3f9e894aa0b5b25 (patch) | |
| tree | f31dca1bcca6b2c9fb3df6a6c1e8dc9f23624d7f /Makefile.ci | |
| parent | 87c959542e1bed55b14d371f1be02cd60d89082c (diff) | |
[ci] Add a default target to `Makefile.ci`
So we avoid problems like the one in #7438.
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/Makefile.ci b/Makefile.ci index 78fec466cd..4d4f1df59a 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 |