diff --git a/.github/workflows/pr-check-on-head-branch.yml b/.github/workflows/pr-check-on-head-branch.yml index 62d762d72f..adb884d62c 100644 --- a/.github/workflows/pr-check-on-head-branch.yml +++ b/.github/workflows/pr-check-on-head-branch.yml @@ -78,8 +78,19 @@ jobs: if [[ ! "$BASE_SHA" =~ ^[0-9a-f]{40}$ || ! "$SINCE" =~ ^[0-9]+$ ]]; then stop "the master diff check reported no base commit, so nothing was merged or compiled" fi - git fetch --no-tags --no-write-fetch-head --shallow-since="$SINCE" origin "$HEAD_SHA" "$BASE_SHA" || + # A shallow fetch starts a background maintenance run that rewrites .git/shallow, and the second shallow fetch + # below then fails with "shallow file has changed since we read it". + fetch() { + git -c maintenance.auto=false -c gc.auto=0 fetch --no-tags --no-write-fetch-head "$@" origin "$HEAD_SHA" "$BASE_SHA" + } + fetch --shallow-since="$SINCE" || stop "the base commit $BASE_SHA could not be fetched, so nothing was merged or compiled" + # A time window records a merge commit itself as shallow when one of its parents predates the window, which + # drops the other, in-window parent too; a depth bound keeps both parents of every commit it covers. + if ! git merge-base "$HEAD_SHA" "$BASE_SHA" >/dev/null; then + fetch --depth=20 --filter=blob:none || + stop "the base commit $BASE_SHA could not be fetched, so nothing was merged or compiled" + fi git -c user.name=pr-check -c user.email=pr-check@users.noreply.github.com merge --no-ff --no-edit -m "Merge $BASE_SHA into $HEAD_SHA" "$BASE_SHA" || stop "the pull request cannot merge $BASE_SHA; merge master into it and push, then this check runs again" echo "merged=true" >> "$GITHUB_OUTPUT"