Skip to content

Commit

Permalink
chore: when setting up Mathlib CI, make sure nightly-with-mathlib bra…
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em authored Apr 5, 2024
1 parent f31c395 commit 0aa6831
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions .github/workflows/pr-release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -149,6 +149,7 @@ jobs:
echo "but 'git merge-base origin/master HEAD' reported: $MERGE_BASE_SHA"
git -C lean4.git log -10 origin/master
git -C lean4.git fetch origin nightly-with-mathlib
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
Expand Down

0 comments on commit 0aa6831

Please sign in to comment.