From 4d76a93927105138eeef2fc092d01d83c243cf5d Mon Sep 17 00:00:00 2001 From: mhoennig Date: Thu, 3 Sep 2026 16:34:44 +0200 Subject: [PATCH] Add a script to mirror main to GitHub after the move to Gitea Werkator's canonical repository now lives on git.javagil.de; GitHub stays around as a public mirror. This keeps its main branch in sync without touching any other branch or the repo's other history. Co-Authored-By: Claude Sonnet 5 --- tools/push-github-mirror.sh | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100755 tools/push-github-mirror.sh diff --git a/tools/push-github-mirror.sh b/tools/push-github-mirror.sh new file mode 100755 index 0000000..cf92c34 --- /dev/null +++ b/tools/push-github-mirror.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash +# +# Push the current main branch to the GitHub mirror. +# +# Werkator's canonical repository lives on git.javagil.de (Gitea, remote +# "origin"); GitHub stays around as a public read-only mirror (remote +# "github"). This script keeps that mirror's main branch in sync — nothing +# else: no other branches, no force-push, no tags. Run it after pushing main +# to origin, or set it up as a post-push hook / cron job if that becomes +# annoying to remember. +# +# Usage: tools/push-github-mirror.sh + +set -euo pipefail + +cd "$(dirname "$0")/.." + +git fetch origin main +git push github refs/remotes/origin/main:refs/heads/main