diff options
| author | Maxime Dénès | 2017-02-07 14:22:08 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-02-07 14:22:08 +0100 |
| commit | 0a1c83768a6b0199afa1ad4fb633c9ede4a84d20 (patch) | |
| tree | 0b39e900ef744160b8c453bb9f5f017c5d3a8039 /Makefile.ci | |
| parent | e61e83758e129d455d664b65a1fe15ecac793186 (diff) | |
| parent | 2a59cdce8c142d451988709a3939b884c63993c9 (diff) | |
Merge PR#421: [travis] Perform parallel testing
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci new file mode 100644 index 0000000000..040144e6e8 --- /dev/null +++ b/Makefile.ci @@ -0,0 +1,10 @@ +CI_TARGETS=ci-all ci-hott ci-math-comp ci-compcert ci-sf ci-cpdt \ + ci-color ci-math-classes ci-tlc ci-fiat-crypto \ + ci-coquelicot ci-flocq ci-iris-coq ci-metacoq ci-geocoq + +.PHONY: $(CI_TARGETS) + +# Generic rule, we use make to easy travis integraton with mixed rules +$(CI_TARGETS): ci-%: + ./dev/ci/ci-$*.sh + |