aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rwxr-xr-xdev/ci/ci-basic-overlay.sh2
-rwxr-xr-xdev/ci/ci-iris.sh4
2 files changed, 0 insertions, 6 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 4799755b15..67555da0a2 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -79,8 +79,6 @@ project iris "https://gitlab.mpi-sws.org/iris/iris" ""
project autosubst "https://github.com/coq-community/autosubst" "master"
-project iris_string_ident "https://gitlab.mpi-sws.org/iris/string-ident" "master"
-
project iris_examples "https://gitlab.mpi-sws.org/iris/examples" "master"
########################################################################
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh
index d29e6f1635..7a72462758 100755
--- a/dev/ci/ci-iris.sh
+++ b/dev/ci/ci-iris.sh
@@ -5,7 +5,6 @@ ci_dir="$(dirname "$0")"
# Setup iris_examples and separate dependencies first
git_download autosubst
-git_download iris_string_ident
git_download iris_examples
# Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
@@ -31,8 +30,5 @@ git_download stdpp
# Build autosubst
( cd "${CI_BUILD_DIR}/autosubst" && make && make install )
-# Build iris-string-ident
-( cd "${CI_BUILD_DIR}/iris_string_ident" && make && make install )
-
# Build Iris examples
( cd "${CI_BUILD_DIR}/iris_examples" && make && make install )