diff options
| author | Gaëtan Gilbert | 2018-05-07 13:16:41 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-05-07 13:16:41 +0200 |
| commit | bb974290e7d05f1b1159c3add9f68f923ab4e1c4 (patch) | |
| tree | e4a0b3024ffb94c20ebe1bf48d7e70f544761c9e | |
| parent | 401e278be6e1f95d1175c5bcb1e33674074988dd (diff) | |
| parent | b0cd4a2db46f8051ffdf9001f3f9e894aa0b5b25 (diff) | |
Merge PR #7440: [ci] Add a default target 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 |