chore(docs): GitHub repo URLs, remove .cursor from git, mirror scripts

Co-authored-by: Cursor <cursoragent@cursor.com>
This commit is contained in:
PTah
2026-06-16 11:36:51 +10:00
parent 9a3855bf0a
commit 2956d14d94
16 changed files with 216 additions and 198 deletions
+43
View File
@@ -0,0 +1,43 @@
#!/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"