diff --git a/prepare-opam.sh b/prepare-opam.sh index 77f56e823986f51c6f7f5c31a98058a1bf64fb6c..475def8d673ee204b5e4ea9c3ab0aea453a4ba8c 100644 --- a/prepare-opam.sh +++ b/prepare-opam.sh @@ -40,7 +40,8 @@ test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-s echo # We really want to run all of the following in one opam transaction, but due to opam limitations, -# that is not currently possible. +# that is not currently possible. Once we use opam 2 for CI, we can first do all the pinning (with `-n`) +# followed by `opam upgrade --all build-dep/` (and hope this will also --fixup). # Install fixed versions of some dependencies. echo_color "$BOLDGREEN" "[prepare-opam] Processing pins"