#!/usr/bin/env bash # Push main to a mirror remote with host-specific doc URLs, without leaving URL churn on main. # Usage: push-mirror.sh github|kalinamall|papatramp set -euo pipefail TARGET="${1:?usage: push-mirror.sh github|kalinamall|papatramp}" ROOT="$(cd "$(dirname "$0")/.." && pwd)" cd "$ROOT" case "$TARGET" in github) REMOTE=github ;; kalinamall) REMOTE=kalinamall ;; papatramp) REMOTE=papatramp ;; *) echo "unknown target: $TARGET" >&2 exit 1 ;; esac if ! git remote get-url "$REMOTE" >/dev/null 2>&1; then echo "remote not configured: $REMOTE" >&2 exit 1 fi if ! git diff --quiet || ! git diff --cached --quiet; then echo "working tree not clean; commit or stash first" >&2 exit 1 fi BEFORE="$(git rev-parse HEAD)" bash "$ROOT/scripts/rewrite-git-host-urls.sh" "$TARGET" if git diff --quiet; then echo "no URL changes for $TARGET; pushing as-is" git push "$REMOTE" main exit 0 fi git add -A git commit -m "chore(docs): sync repository URLs for ${TARGET} mirror" git push "$REMOTE" main git reset --hard "$BEFORE" echo "pushed $REMOTE with ${TARGET} URLs; local main reset to $BEFORE"