Skip to content

Commit

Permalink
chore: fix rebase suggestion for Mathlib CI (#3701)
Browse files Browse the repository at this point in the history
Previously we were suggesting rebasing onto the most recently nightly in
the branches history, but that is incorrect and we should *always*
suggest rebasing on `origin/nightly-with-mathlib`.

---------

Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
  • Loading branch information
semorrison and nomeata committed Mar 27, 2024
1 parent 70924be commit 5b7ec44
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion .github/workflows/pr-release.yml
Expand Up @@ -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
Expand Down

0 comments on commit 5b7ec44

Please sign in to comment.