diff options
| author | Théo Zimmermann | 2019-08-20 13:38:59 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-20 13:38:59 +0200 |
| commit | 60f0b23aaf176fcc319455677c6c678b980ee3de (patch) | |
| tree | 4e59f086d20c51c0be2b5031ccfd4028bdaa4eec /Makefile.ci | |
| parent | 92f38826f767db01dbc51f2372b23e7b4e3b1aaa (diff) | |
[ci] Remove dead code.
TLC and CPDT are not actually tested. No point in keeping them as if they were.
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/Makefile.ci b/Makefile.ci index 677fd734bf..de03ee8e84 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -18,7 +18,6 @@ CI_TARGETS= \ ci-coq_dpdgraph \ ci-coquelicot \ ci-corn \ - ci-cpdt \ ci-cross-crypto \ ci-elpi \ ci-ext-lib \ @@ -41,7 +40,6 @@ CI_TARGETS= \ ci-sf \ ci-simple-io \ ci-stdlib2 \ - ci-tlc \ ci-unimath \ ci-verdi-raft \ ci-vst |