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

Author: Kha

.github/workflows/pr-release.yml

@@ -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