From 40b71102efe051c777a785035aebcbaa4c2ec19f Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Tue, 24 Apr 2018 21:13:53 +0200
Subject: [PATCH] lay down opam 2 plans

---
 prepare-opam.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/prepare-opam.sh b/prepare-opam.sh
index 77f56e8..475def8 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"
-- 
GitLab