diff options
| author | coqbot-app[bot] | 2020-11-12 14:33:06 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-12 14:33:06 +0000 |
| commit | 7ba09858a87a6940278c96ae328e44c142842cd9 (patch) | |
| tree | 31c1a0a2bed13bae0b3e718cbd1dd7717f9f4000 /dev | |
| parent | 24140636aa5562ba2dee407127339be1c96f4293 (diff) | |
| parent | 18db1c084c969c898c7fb5aaee101f406d38da4d (diff) | |
Merge PR #13355: Fix Iris CI script
Reviewed-by: ejgallego
Ack-by: RalfJung
Ack-by: Zimmi48
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-iris.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh index 9616f3ce00..d29e6f1635 100755 --- a/dev/ci/ci-iris.sh +++ b/dev/ci/ci-iris.sh @@ -9,13 +9,15 @@ git_download iris_string_ident git_download iris_examples # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *) -iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +iris_CI_REF=$(grep -F '"coq-iris-heap-lang"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +[ -n "$iris_CI_REF" ] || { echo "Could not find Iris dependency version" && exit 1; } # Setup Iris git_download iris # Extract required version of std++ stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/coq-iris.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +[ -n "$stdpp_CI_REF" ] || { echo "Could not find stdpp dependency version" && exit 1; } # Setup std++ git_download stdpp |