2020-09-05 20:34:23 +00:00
|
|
|
#!/bin/bash
|
|
|
|
|
set -xe
|
|
|
|
|
REPO="$1"
|
|
|
|
|
REF="$2"
|
|
|
|
|
DEST="$3"
|
|
|
|
|
git init "$DEST"
|
|
|
|
|
git -C "$DEST" remote add origin "$REPO"
|
2022-01-04 18:49:05 +00:00
|
|
|
|
2022-07-12 23:46:13 +00:00
|
|
|
retry-tool git -C "$DEST" fetch --depth=1 origin "$REF"
|
2022-01-04 18:49:05 +00:00
|
|
|
|
2020-09-05 20:34:23 +00:00
|
|
|
git -C "$DEST" config advice.detachedHead false
|
|
|
|
|
git -C "$DEST" checkout FETCH_HEAD
|
