diff options
| author | Ralf Jung | 2020-09-02 16:34:39 +0200 |
|---|---|---|
| committer | Ralf Jung | 2020-09-02 16:34:39 +0200 |
| commit | eec818eb30876727d31c9aa727be842578244d26 (patch) | |
| tree | e2c0e9c87edf04b79a13542c014d3792baf4df02 /dev/ci | |
| parent | 2d5a04e0f276613563406f1d6a2af9955ba11b55 (diff) | |
fix grepping for the Iris commit
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-iris.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh index 93ec2233d3..0256906112 100755 --- a/dev/ci/ci-iris.sh +++ b/dev/ci/ci-iris.sh @@ -9,13 +9,13 @@ 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/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup Iris git_download iris # Extract required version of std++ -stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') +stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/') # Setup std++ git_download stdpp |