From 18db1c084c969c898c7fb5aaee101f406d38da4d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 11 Nov 2020 21:08:15 +0100
Subject: Fix Iris CI script

Also add nice error message when the grep produces an empty result
---
 dev/ci/ci-iris.sh | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

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
-- 
cgit v1.2.3