Improve mirror-to-github documentation

mirror-to-github

@@ -1,5 +1,8 @@
 #!/usr/local/bin/bash
-# $1= destination repository, including tokens
+# 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")"
@@ -8,9 +11,10 @@ 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 ]]  dst: '[redacted]'"
 echo "[[ Deploy ]]  tmp: '$tmp_dir'"
 
+
 if test -e "$tmp_dir"; then
     echo "[[ Deploy ]]  Directory '$tmp_dir' already exists, stopping deployment."
     exit