chore: update batteries in manifest when creating lean-pr-testing-NNN…

…N at Mathlib (#4333)
leanprover · Jun 4, 2024 · 05ea3ac · 05ea3ac
1 parent a54fa7c
commit 05ea3ac
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml
@@ -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."