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

chore: when bumping Mathlib testing branches, bump to latest nightly-testing (#2553)

Browse source
This commit is contained in:
Scott Morrison 2023-09-18 12:02:24 +10:00 • committed by GitHub
parent ee3ac9901e
commit c4bd112a7f
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -110,6 +110,11 @@ jobs:
else
echo "Branch already exists, pushing an empty commit."
git checkout lean-pr-testing-${{ steps.workflow-info.outputs.pullRequestNumber }}
# The Mathlib `nightly-testing` branch may have moved since this branch was created, so merge their changes.
# If the base of this Lean4 PR becomes significantly older than the nightly being used by `nightly-testing`
# this will cause breakages rather than fixing them!
# Without cumbersome requirements that Lean4 PRs are based off nightlies, I'm not sure there is a perfect solution here.
git merge nightly-testing --strategy-option ours --no-commit --allow-unrelated-histories
git commit --allow-empty -m "Trigger CI for https://github.com/leanprover/lean4/pull/${{ steps.workflow-info.outputs.pullRequestNumber }}"
fi