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

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

Browse source 
This reverts commit 12ad957bd5.
This commit is contained in:
Sebastian Ullrich 2026-02-09 13:12:12 +00:00
parent 5ba467d920
commit b4a254de69
1 changed files with 1 additions and 2 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,8 +61,7 @@ jobs:
run: |
git init --bare lean4.git
git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
# 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 master
git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
# Create both the original tag and the SHA-suffixed tag