diff options
| author | Maxime Dénès | 2017-10-20 11:14:09 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-20 11:14:09 +0200 |
| commit | 62684a5c817da4afc2a7dac6ece03facabdd5fe4 (patch) | |
| tree | 224a8c854062bcd75add73f0a95a40223239acd1 /dev/ci/ci-basic-overlay.sh | |
| parent | 025a60b92618e4a8f10ab9704a38949383c87efa (diff) | |
| parent | 8df509882d5b0954b40b576c4e9d3b3f742c619d (diff) | |
Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just Iris
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 43525dcd40..545846da58 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -43,6 +43,9 @@ : ${Iris_CI_BRANCH:=master} : ${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/FP/iris-coq.git} +: ${lambdaRust_CI_BRANCH:=master} +: ${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/FP/LambdaRust-coq.git} + ######################################################################## # HoTT ######################################################################## |