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

chore: pr release: git commit --allow-empty (#11013)

Browse source 
This PR uses `--allow-empty` so that the PR release script does not fail
when it's being retried after an intermittent failure.
This commit is contained in:
Joachim Breitner 2025-10-29 16:48:11 -04:00 • committed by GitHub
parent 1587d02dfb
commit 2f0f0a3018
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -426,7 +426,7 @@ jobs:
git switch -c lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }} "$BASE"
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
git add lean-toolchain
git commit -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, updating lean-toolchain."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
@ -435,7 +435,7 @@ jobs:
git merge "$BASE" --strategy-option ours --no-commit --allow-unrelated-histories
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
git add lean-toolchain
git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi
- name: Push changes
@ -496,7 +496,7 @@ jobs:
sed -i 's,require "leanprover-community" / "batteries" @ git ".\+",require "leanprover-community" / "batteries" @ git "lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}",' 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 }}"
git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, updating lean-toolchain and bumping Batteries."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
@ -507,7 +507,7 @@ jobs:
git add lean-toolchain
lake update batteries
git add lake-manifest.json
git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi
- name: Push changes
@ -558,7 +558,7 @@ jobs:
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
git add lean-toolchain
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 }}"
git commit --allow-empty -m "Update lean-toolchain for testing https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
else
echo "Branch already exists, updating lean-toolchain."
git switch lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
@ -568,7 +568,7 @@ jobs:
echo "leanprover/lean4-pr-releases:pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-${{ env.SHORT_SHA }}" > lean-toolchain
git add lean-toolchain
git add lake-manifest.json
git commit -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
git commit --allow-empty -m "Update lean-toolchain for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi
- name: Push changes