diff options
| author | Maxime Dénès | 2018-02-21 19:05:57 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-21 19:05:57 +0100 |
| commit | cec85230d0a6c8c546d3297d6108917f7a3157e7 (patch) | |
| tree | 303cb5781d75cda6994b6eefa826093ca567228e /Makefile.ci | |
| parent | 4b0fe4e09d547f0e6ee98da3fd6f7a134e51f3fd (diff) | |
| parent | 1dcf5516ab772a6d5325d42c2ceaf727fe88bb86 (diff) | |
Merge PR #6767: [ci] add elpi
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.ci b/Makefile.ci index 80fbd7bbe1..4e92264d62 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -5,6 +5,7 @@ CI_TARGETS=ci-bignums \ ci-coquelicot \ ci-corn \ ci-cpdt \ + ci-elpi \ ci-equations \ ci-fiat-crypto \ ci-fiat-parsers \ |