diff options
| author | Ralf Jung | 2020-09-02 15:40:28 +0200 |
|---|---|---|
| committer | Ralf Jung | 2020-09-02 15:43:18 +0200 |
| commit | 2d5a04e0f276613563406f1d6a2af9955ba11b55 (patch) | |
| tree | fca7a4038753d182981f457a3934a805dd6b25f7 /Makefile.ci | |
| parent | cc51e1fd680c1f1bf47cc8b504196c9f2677fa3b (diff) | |
CI: build Iris examples instead of lambda-Rust
Diffstat (limited to 'Makefile.ci')
| -rw-r--r-- | Makefile.ci | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.ci b/Makefile.ci index 85e4b965f9..af78f252df 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -37,7 +37,7 @@ CI_TARGETS= \ ci-geocoq \ ci-coqhammer \ ci-hott \ - ci-lambda_rust \ + ci-iris \ ci-math_classes \ ci-mathcomp \ ci-metacoq \ |