diff options
| author | Maxime Dénès | 2019-01-04 16:13:29 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-04 16:15:56 +0100 |
| commit | 302e42331060865b2804e3de8ee87256917983cc (patch) | |
| tree | 1e885defc82ba4eacd9aca2f87a1040f3078f888 /Makefile.ci | |
| parent | 0a5bbf347b5bbcb579f94eb3d0166778cd92cfdb (diff) | |
Remove formal-topology from CI
This was suggested by the author. See
https://github.com/bmsherman/topology/issues/23
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Makefile.ci b/Makefile.ci index 2df6a792b6..6805304f55 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -27,7 +27,6 @@ CI_TARGETS= \ ci-fiat-crypto-legacy \ ci-fiat-parsers \ ci-flocq \ - ci-formal-topology \ ci-geocoq \ ci-coqhammer \ ci-hott \ @@ -63,8 +62,6 @@ ci-corn: ci-math-classes ci-simple-io: ci-ext-lib ci-quickchick: ci-ext-lib ci-simple-io -ci-formal-topology: ci-corn - # Generic rule, we use make to ease CI integration $(CI_TARGETS): ci-%: +./dev/ci/ci-wrapper.sh $* |