opam-pins.sh 866 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
2
3
4
5
6
#!/bin/bash
set -e
## Process an opam.pins file from stdin: Add all the given pins, but don't install anything.
## Usage:
##   ./opam-pins.sh < opam.pins

Ralf Jung's avatar
Ralf Jung committed
7
8
9
10
11
if ! which curl >/dev/null; then
    echo "opam-pins needs curl. Please install curl and try again."
    exit 1
fi

Ralf Jung's avatar
Ralf Jung committed
12
13
14
15
16
# Process stdin
while read PACKAGE URL HASH; do
    if echo "$URL" | egrep '^https://gitlab\.mpi-sws\.org' > /dev/null; then
        echo "[opam-pins] Recursing into $URL"
        # an MPI URL -- try doing recursive pin processing
Ralf Jung's avatar
Ralf Jung committed
17
        curl -f "$URL/raw/$HASH/opam.pins" 2>/dev/null | "$0"
Ralf Jung's avatar
Ralf Jung committed
18
    fi
19
20
21
22
23
    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
Ralf Jung's avatar
Ralf Jung committed
24
        echo
25
    fi
Ralf Jung's avatar
Ralf Jung committed
26
done