chore: commit lake-manifest.json when updating lean-pr-testing branches

2026-03-31 01:04:07 +00:00 · 2024-09-27 16:33:23 +10:00
1 changed files with 1 additions and 0 deletions
--- a/.github/workflows/pr-release.yml
+++ b/.github/workflows/pr-release.yml
@@ -340,6 +340,7 @@ jobs:
            # (This should no longer be possible once `nightly-testing-YYYY-MM-DD` is a tag, but it is still safe to merge.)
            git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
            lake update batteries
+            get add lake-manifest.json
            git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
          fi