diff options
author | tv <tv@krebsco.de> | 2015-05-21 01:56:08 +0200 |
---|---|---|
committer | tv <tv@krebsco.de> | 2015-05-21 01:56:08 +0200 |
commit | 60e526dc9419d0bff89b05f4a98332aae48a0253 (patch) | |
tree | 484cb2c1075cdcabe8020ca40704f4d68f2b2fed /bin/ssh-fetch-git | |
parent | 6b976a36f5ef72d7463f848b55f250b807291bfd (diff) |
sh: functions -> bin/
Diffstat (limited to 'bin/ssh-fetch-git')
-rwxr-xr-x | bin/ssh-fetch-git | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/bin/ssh-fetch-git b/bin/ssh-fetch-git new file mode 100755 index 0000000..7de58ab --- /dev/null +++ b/bin/ssh-fetch-git @@ -0,0 +1,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 |