From 353e11f7617be9a0d9d35299c82881f9ffaa4f9b Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 4 Jun 2024 09:32:59 +1000 Subject: [PATCH] chore: update batteries in manifest when creating lean-pr-testing-NNNN at Mathlib --- .github/workflows/pr-release.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/pr-release.yml b/.github/workflows/pr-release.yml index 1c15eda08e9a..80ddb55808e4 100644 --- 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."