From 9d9158d4686aa4c01957e0f68564de4cd9451d77 Mon Sep 17 00:00:00 2001 From: JKRT Date: Wed, 28 Oct 2026 21:14:19 +0100 Subject: [PATCH] Coverage: publish onto the branch's current head A dispatched run checks out the commit the branch had when the run was queued. When another coverage run's docs commit landed in the meantime (runs wait in the concurrency group), the docs push was rejected as a non-fast-forward and the site step skipped. Publish now writes the README section into the branch's current README, and the docs commit goes on that head with only README.md and the version's coverage page. Assisted-by: Claude Opus 5.5 --- .github/workflows/coverage.yml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/.github/workflows/coverage.yml b/.github/workflows/coverage.yml index aaa188a..436b04e 100644 --- a/.github/workflows/coverage.yml +++ b/.github/workflows/coverage.yml @@ -225,6 +225,10 @@ jobs: id: publish working-directory: OM.jl/OMLibraryTesting.jl run: | + # The README as the branch has it now, not as it was when the run was queued: another + # run's documentation commit may have landed since (runs wait in the concurrency group). + git fetch -q origin "${GITHUB_REF_NAME}" + git checkout -q FETCH_HEAD -- README.md results=$(ls -t logs/partial_ci_*.jls | head -1) julia --color=yes --project=. scripts/publish_coverage.jl "$results" "$GITHUB_WORKSPACE/commits.txt" "$NOTE" cat "$COVERAGE_MD" >> "$GITHUB_STEP_SUMMARY" @@ -247,6 +251,8 @@ jobs: run: | git config user.name "github-actions[bot]" git config user.email "41898282+github-actions[bot]@users.noreply.github.com" + # On the branch's head as fetched for Publish: its files, this run's page and README section. + git reset -q FETCH_HEAD git add README.md "$COVERAGE_MD" if git diff --cached --quiet; then echo "Coverage unchanged"; exit 0; fi git commit -m "Coverage of $(date -u +%Y-%m-%d), MSL $MSL [skip ci]"