diff options
| author | Gaëtan Gilbert | 2020-02-12 13:27:12 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 22:12:47 +0100 |
| commit | 33efbc7d6f09618255a6047d35d2b9035805dd41 (patch) | |
| tree | dd4a95f9b8685d6cd9dd9fbce291ff23b30fd2fb /Makefile.ci | |
| parent | 9700c44dca70f5550a6713e4ccbb3693e058a9a7 (diff) | |
Split unicoq out of ci-mtac2.sh (keeping 1 CI job)
No reason to have them in the same .sh
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci index f14203fa4a..c2a3cd7e14 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -45,6 +45,7 @@ CI_TARGETS= \ ci-stdlib2 \ ci-tlc \ ci-unimath \ + ci-unicoq \ ci-verdi-raft \ ci-vst @@ -64,6 +65,8 @@ ci-math-classes: ci-bignums ci-corn: ci-math-classes +ci-mtac2: ci-unicoq + ci-fiat-crypto: ci-coqprime ci-rewriter ci-simple-io: ci-ext-lib |