1 files changed, 0 insertions, 35 deletions
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