diff options
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/ci/ci-iris-coq.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-iris-coq.sh b/dev/ci/ci-iris-coq.sh index 4347da1da4..c49b6ed9c9 100755 --- a/dev/ci/ci-iris-coq.sh +++ b/dev/ci/ci-iris-coq.sh @@ -21,7 +21,7 @@ stdpp_URL=$(opam show coq-stdpp.$stdpp_VERSION -f upstream-url) read -a stdpp_URL_PARTS <<< $(echo $stdpp_URL | tr '#' ' ') # Setup std++ -git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[1]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[2]} +git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_URL_PARTS[1]} ( cd ${stdpp_CI_DIR} && make && make install ) # Build iris now |