From 19f07d9153e77dead1722360a0a8461cfdcb1570 Mon Sep 17 00:00:00 2001
From: "Florine W. Dekker" <florine@fwdekker.com>
Date: Mon, 28 Feb 2022 17:53:29 +0100
Subject: [PATCH] Remove now-unused mirror-to-github script

---
 mirror-to-github | 28 ----------------------------
 1 file changed, 28 deletions(-)
 delete mode 100755 mirror-to-github

diff --git a/mirror-to-github b/mirror-to-github
deleted file mode 100755
index f44ff78..0000000
--- a/mirror-to-github
+++ /dev/null
@@ -1,28 +0,0 @@
-#!/usr/local/bin/bash
-# $1= destination repository, including tokens
-
-repo_url="$(pwd)"
-repo_name="$(basename -s .git "$repo_url")"
-dst_url="$1"
-tmp_dir="$HOME/tmp/git/$repo_name-$(date +%s)"
-
-echo "[[ Deploy ]]  mirror-to-github($repo_name)"
-echo "[[ Deploy ]]  src: '$repo_url'"
-echo "[[ Deploy ]]  dst: '$dst_url'"
-echo "[[ Deploy ]]  tmp: '$tmp_dir'"
-
-if test -e "$tmp_dir"; then
-    echo "[[ Deploy ]]  Directory '$tmp_dir' already exists, stopping deployment."
-    exit
-fi
-
-
-echo "[[ Deploy ]]  Bare cloning repository at '$repo_url' into '$tmp_dir'."
-git clone --bare "$repo_url" "$tmp_dir"
-
-echo "[[ Deploy ]]  Mirroring repo at '$tmp_dir' into '$dst_url'."
-cd "$tmp_dir" || exit
-git push --mirror "$dst_url"
-
-echo "[[ Deploy ]]  Deleting '$tmp_dir'."
-rm -rf "$tmp_dir"