From b9ef84b4ead589937f83f12ce92725da5a5af06e Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Fri, 3 Nov 2017 12:05:49 +0100 Subject: [PATCH] try to work around yet another opam silliness --- build/opam-ci.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build/opam-ci.sh b/build/opam-ci.sh index 66ccfc94..b6925ba5 100755 --- a/build/opam-ci.sh +++ b/build/opam-ci.sh @@ -55,7 +55,7 @@ done # Upgrade cached things. echo echo "[opam-ci] Upgrading opam" -opam upgrade -y --fixup +opam upgrade -y --fixup && opam upgrade -y # Install build-dependencies. echo -- GitLab