From f0b8ee664db3a37efabf3ed1ed32febacd8e6370 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Oct 2017 10:44:30 +0200
Subject: [PATCH] don't try to be smart about having an up-to-date opam
---
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 95abf4bc0..bcd79ee4e 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