Revert "Remove now-unused mirror-to-github script"

This reverts commit 19f07d9153.
This commit is contained in:
Florine W. Dekker 2023-01-31 12:32:58 +01:00
parent d944381311
commit 9afa3e1779
Signed by: FWDekker
GPG Key ID: D3DCFAA8A4560BE0
1 changed files with 28 additions and 0 deletions

28
mirror-to-github Executable file
View File

@ -0,0 +1,28 @@
#!/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"