From b6d6097997fb54594e88187cfbee2b65b2edc385 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 28 Oct 2017 15:29:51 +0200
Subject: [PATCH] stop being smart about updating opam, it doesn't work very
well
---
build/opam-ci.sh | 9 ++-------
1 file changed, 2 insertions(+), 7 deletions(-)
diff --git a/build/opam-ci.sh b/build/opam-ci.sh
index 95abf4bc..bcd79ee4 100755
--- a/build/opam-ci.sh
+++ b/build/opam-ci.sh
@@ -19,13 +19,8 @@ eval `opam conf env`
run_and_print make build-dep/opam
# Update repositories
-if test $(find "$OPAMROOT/repo/package-index" -mtime +0); then
- # last update was more than a day ago
- run_and_print opam update
-else
- # only update iris-dev, and only if it already exists
- if test -d "$OPAMROOT/repo/iris-dev"; then run_and_print opam update iris-dev; fi
-fi
+run_and_print opam update
+
# Make sure we got the right set of repositories registered
if echo "$@" | fgrep "dev"; then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
--
GitLab