max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: find nightly-with-mathlib SHA (#3923)

Browse source
This commit is contained in:
Kim Morrison 2024-04-16 13:18:51 +02:00 • committed by GitHub
parent 23aacdeac0
commit a8df7d9d5c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/pr-release.yml vendored
View file

@ -150,7 +150,7 @@ jobs:
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")"
NIGHTLY_WITH_MATHLIB_SHA="$(git -C lean4.git rev-parse "origin/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