diff options
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/Makefile.ci b/Makefile.ci index 334827a937..3c26bf964b 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -1,11 +1,21 @@ -CI_TARGETS=ci-all \ - ci-bignums \ +########################################################################## +## # The Coq Proof Assistant / The Coq Development Team ## +## v # INRIA, CNRS and contributors - Copyright 1999-2018 ## +## <O___,, # (see CREDITS file for the list of authors) ## +## \VV/ ############################################################### +## // # This file is distributed under the terms of the ## +## # GNU Lesser General Public License Version 2.1 ## +## # (see LICENSE file for the text of the license) ## +########################################################################## + +CI_TARGETS=ci-bignums \ ci-color \ ci-compcert \ ci-coq-dpdgraph \ ci-coquelicot \ ci-corn \ ci-cpdt \ + ci-elpi \ ci-equations \ ci-fiat-crypto \ ci-fiat-parsers \ @@ -23,7 +33,7 @@ CI_TARGETS=ci-all \ ci-unimath \ ci-vst -.PHONY: $(CI_TARGETS) +.PHONY: ci-all $(CI_TARGETS) ci-color: ci-bignums @@ -37,6 +47,8 @@ ci-formal-topology: ci-corn $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* +ci-all: $(CI_TARGETS) + # For emacs: # Local Variables: # mode: makefile |