From f8b1e849a6a3bd53f24a4aac70bc904cdb5ff711 Mon Sep 17 00:00:00 2001
From: tv <tv@shackspace.de>
Date: Thu, 21 May 2015 23:52:06 +0200
Subject: deploy: merge next

---
 bin/ssh-fetch-git | 35 -----------------------------------
 1 file changed, 35 deletions(-)
 delete mode 100755 bin/ssh-fetch-git

(limited to 'bin/ssh-fetch-git')

diff --git a/bin/ssh-fetch-git b/bin/ssh-fetch-git
deleted file mode 100755
index 7de58ab73..000000000
--- a/bin/ssh-fetch-git
+++ /dev/null
@@ -1,35 +0,0 @@
-#! /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
-- 
cgit v1.2.3