Skip to content
Snippets Groups Projects
Commit c3027327 authored by Ralf Jung's avatar Ralf Jung
Browse files

opam-pins: avoid re-downloading already properly pinned packages

parent 5a475f3a
No related branches found
No related tags found
No related merge requests found
Pipeline #
...@@ -11,7 +11,11 @@ while read PACKAGE URL HASH; do ...@@ -11,7 +11,11 @@ while read PACKAGE URL HASH; do
# an MPI URL -- try doing recursive pin processing # an MPI URL -- try doing recursive pin processing
curl -f "$URL/raw/$HASH" 2> /dev/null | "$0" curl -f "$URL/raw/$HASH" 2> /dev/null | "$0"
fi fi
echo "[opam-pins] Applying pin: $PACKAGE -> $URL#$HASH" if opam pin list | fgrep "$PACKAGE.dev.$HASH " > /dev/null; then
opam pin add "$PACKAGE.dev.$HASH" "$URL#$HASH" -k git -y -n 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 echo
done done
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment