blob: 7de58ab73220283fc40415a68755c38a5d1ec872 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
#! /bin/sh
# ssh-fetch-git : [user@]hostname x remote_dir x git_url x git_rev -> ()
set -euf
target=$1
remote_dir=$2
git_url=$3
git_rev=$4
echo '
set -euf
if [ ! -d "$remote_dir" ]; then
mkdir -p "$remote_dir"
fi
cd "$remote_dir"
git init -q
if ! current_url=$(git config remote.src.url); then
git remote add src "$git_url"
elif [ $current_url != $git_url ]; then
git remote set-url src "$git_url"
fi
git fetch src
git checkout "$git_rev"
' \
| ssh "$target" env \
remote_dir="$remote_dir" \
git_rev="$git_rev" \
git_url="$git_url" \
/bin/sh
|
