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

chore: CI: avoid fetching full repo in PR Release (#12309)

Browse source
This commit is contained in:
Sebastian Ullrich 2026-02-09 06:14:33 +01:00 • committed by GitHub
parent 690648d943
commit 12ad957bd5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -61,7 +61,8 @@ jobs:
run: |
git init --bare lean4.git
git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
git -C lean4.git fetch -n origin master
# we only need to fetch the history; note this flag is sticky
git -C lean4.git fetch -n origin --filter=tree:0 master
git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
# Create both the original tag and the SHA-suffixed tag