diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index a7a084d4e693..f338f76884d3 100644 --- a/.github/workflows/pr-release.yml +++ b/.github/workflows/pr-release.yml @@ -149,7 +149,8 @@ jobs: echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA" git -C lean4.git log -10 origin/master - MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_SHA\`." + NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "nightly-with-mathlib")" + MESSAGE="- ❗ Std/Mathlib CI will not be attempted unless your PR branches off the \`nightly-with-mathlib\` branch. Try \`git rebase $MERGE_BASE_SHA --onto $NIGHTLY_WITH_MATHLIB_SHA\`." fi if [[ -n "$MESSAGE" ]]; then