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

chore: update batteries in manifest when creating lean-pr-testing-NNNN at Mathlib (#4333)

Browse source
This commit is contained in:
Kim Morrison 2024-06-04 02:45:37 +01:00 • committed by GitHub
parent a54fa7cae6
commit 05ea3ac19f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -322,7 +322,8 @@ jobs:
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}" > lean-toolchain
git add lean-toolchain
sed -i "s/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \".\+\"/require batteries from git \"https:\/\/github.com\/leanprover-community\/batteries\" @ \"nightly-testing-${MOST_RECENT_NIGHTLY}\"/" lakefile.lean
git add lakefile.lean
lake update batteries
git add lakefile.lean lake-manifest.json
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, pushing an empty commit."