From c30273277fd954eeb3f4cf1fb52363276d05641b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 Jan 2017 19:01:56 +0100
Subject: [PATCH] opam-pins: avoid re-downloading already properly pinned
packages
---
build/opam-pins.sh | 8 ++++++--
1 file changed, 6 insertions(+), 2 deletions(-)
diff --git a/build/opam-pins.sh b/build/opam-pins.sh
index aebd23ca..669cd99b 100755
--- a/build/opam-pins.sh
+++ b/build/opam-pins.sh
@@ -11,7 +11,11 @@ while read PACKAGE URL HASH; do
# an MPI URL -- try doing recursive pin processing
curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
fi
- echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
- opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+ if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
+ echo "[opam-pins] $PACKAGE already at commit $HASH"
+ else
+ echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH"
+ opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n
+ fi
echo
done
--
GitLab