Improve mirror-to-github documentation

This reverts commit 19f07d9153.

mirror-to-github

@@ -0,0 +1,32 @@
+#!/usr/local/bin/bash
+# Usage: `mirror-to-github $github_auth`
+#
+# Mirrors the entire repository with GitHub. Authentication happens using `$github_auth`, which has the form
+# `https://<username>:<token>@github.com/<username>/<repository>.git`.
+
+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: '[redacted]'"
+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"