From 365c27ac01b04f59912cdba69f66227bcb136ee3 Mon Sep 17 00:00:00 2001 From: igneum-labs <337424239+igneum-labs@users.noreply.github.com> Date: Wed, 7 Oct 2026 18:19:47 +0000 Subject: [PATCH] merge-to-master.sh takes MERGE_REMOTE (default origin): the box mirror's master while GitHub is suspended, 7 October 2026 Co-Authored-By: Claude Fable 5.1 --- tools/ci/merge-to-master.sh | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/tools/ci/merge-to-master.sh b/tools/ci/merge-to-master.sh index 11bb7685b..54462c3b6 100755 --- a/tools/ci/merge-to-master.sh +++ b/tools/ci/merge-to-master.sh @@ -6,9 +6,11 @@ # the full gate on landing. Retries while master moves. Never force; never from a dirty branch. # # tools/ci/merge-to-master.sh [] [--tries N] default: the current branch, 6 tries +# MERGE_REMOTE=box tools/ci/merge-to-master.sh ... land on another remote's master (the box mirror /srv/igneum.git while GitHub is +# suspended, 7 October 2026); the default stays origin set -euo pipefail ROOT=$(git rev-parse --show-toplevel); cd "$ROOT" -BRANCH="$(git rev-parse --abbrev-ref HEAD)"; TRIES=6 +BRANCH="$(git rev-parse --abbrev-ref HEAD)"; TRIES=6; R="${MERGE_REMOTE:-origin}" while [ $# -gt 0 ]; do case "$1" in --tries) TRIES="$2"; shift 2 ;; -*) echo "unknown option $1" >&2; exit 2 ;; *) BRANCH="$1"; shift ;; esac; done [ -z "$(git status --porcelain --untracked-files=no)" ] || { echo "merge-to-master: the tree has uncommitted tracked changes; commit first" >&2; exit 1; } SHA=$(git rev-parse "$BRANCH"); G=$(cd "$(git rev-parse --git-common-dir)" && pwd -P) @@ -19,18 +21,18 @@ if [ ! -f "$G/igneum-gate-green/$SHA" ]; then fi AUTHOR=(-c user.name=igneum-labs -c user.email=337424239+[removed]) for i in $(seq 1 "$TRIES"); do - git fetch -q origin master; TIP=$(git rev-parse origin/master) - if git merge-base --is-ancestor "$SHA" "$TIP"; then echo "merge-to-master: ${SHA:0:8} is already on origin/master $(git log -1 --format=%h origin/master)"; exit 0; fi + git fetch -q "$R" master; TIP=$(git rev-parse "$R/master") + if git merge-base --is-ancestor "$SHA" "$TIP"; then echo "merge-to-master: ${SHA:0:8} is already on $R/master $(git log -1 --format=%h "$R/master")"; exit 0; fi W=$(mktemp -d "${TMPDIR:-/tmp}/merge-to-master.XXXXXX"); rmdir "$W" git worktree add -q --detach "$W" "$TIP" if ( cd "$W" && git "${AUTHOR[@]}" merge -q --no-ff -m "Merge $BRANCH ${SHA:0:8} into master (gate: green on ${SHA:0:8}, recorded by tools/ci/pre-push.sh; the full gate runs in CI on this merge)" "$SHA" ); then - if ( cd "$W" && git push -q origin HEAD:master ); then - git worktree remove --force "$W"; git fetch -q origin master - echo "merge-to-master: pushed on try $i: origin/master $(git log -1 --format='%h %ci' origin/master) $(TZ=Europe/London date '+%H:%M %Z')"; exit 0 + if ( cd "$W" && git push -q "$R" HEAD:master ); then + git worktree remove --force "$W"; git fetch -q "$R" master + echo "merge-to-master: pushed on try $i: $R/master $(git log -1 --format='%h %ci' "$R/master") $(TZ=Europe/London date '+%H:%M %Z')"; exit 0 fi echo "merge-to-master: try $i: the push was rejected (master moved or the hook was red); again" else - echo "merge-to-master: the merge of $BRANCH onto ${TIP:0:8} does not apply cleanly; resolve on the branch (git merge origin/master) and retry" >&2 + echo "merge-to-master: the merge of $BRANCH onto ${TIP:0:8} does not apply cleanly; resolve on the branch (git merge $R/master) and retry" >&2 git worktree remove --force "$W"; exit 1 fi git worktree remove --force "$W" 2>/dev/null || true