@@ -48,17 +48,17 @@ jobs:
4848 git -C lean4.git remote add origin https://github.com/${{ github.repository_owner }}/lean4.git
4949 git -C lean4.git fetch -n origin master
5050 git -C lean4.git fetch -n origin "${{ steps.workflow-info.outputs.sourceHeadSha }}"
51-
51+
5252 # Create both the original tag and the SHA-suffixed tag
5353 SHORT_SHA="${{ steps.workflow-info.outputs.sourceHeadSha }}"
5454 SHORT_SHA="${SHORT_SHA:0:7}"
55-
55+
5656 # Export the short SHA for use in subsequent steps
5757 echo "SHORT_SHA=${SHORT_SHA}" >> "$GITHUB_ENV"
5858
5959 git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }} "${{ steps.workflow-info.outputs.sourceHeadSha }}"
6060 git -C lean4.git tag -f pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}" "${{ steps.workflow-info.outputs.sourceHeadSha }}"
61-
61+
6262 git -C lean4.git remote add pr-releases https://foo:'${{ secrets.PR_RELEASES_TOKEN }}'@github.com/${{ github.repository_owner }}/lean4-pr-releases.git
6363 git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}
6464 git -C lean4.git push -f pr-releases pr-release-${{ steps.workflow-info.outputs.pullRequestNumber }}-"${SHORT_SHA}"
@@ -200,7 +200,7 @@ jobs:
200200 -H "Accept: application/vnd.github.v3+json" \
201201 "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
202202 | jq -r '.[].name')"
203-
203+
204204 if echo "$LABELS" | grep -q "^force-mathlib-ci$"; then
205205 echo "force-mathlib-ci label detected, forcing CI despite issues"
206206 MESSAGE="Forcing Mathlib CI because the \`force-mathlib-ci\` label is present, despite problem: $MESSAGE"
@@ -301,7 +301,7 @@ jobs:
301301 -H "Accept: application/vnd.github.v3+json" \
302302 "https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/labels" \
303303 | jq -r '.[].name')"
304-
304+
305305 if echo "$LABELS" | grep -q "^force-manual-ci$"; then
306306 echo "force-manual-ci label detected, forcing CI despite issues"
307307 MESSAGE="Forcing reference manual CI because the \`force-manual-ci\` label is present, despite problem: $MESSAGE"
@@ -401,6 +401,7 @@ jobs:
401401 token : ${{ secrets.MATHLIB4_BOT }}
402402 ref : nightly-testing
403403 fetch-depth : 0 # This ensures we check out all tags and branches.
404+ filter : tree:0
404405
405406 - name : Check if tag exists
406407 if : steps.workflow-info.outputs.pullRequestNumber != '' && steps.ready.outputs.mathlib_ready == 'true'
@@ -460,6 +461,7 @@ jobs:
460461 token : ${{ secrets.MATHLIB4_BOT }}
461462 ref : nightly-testing
462463 fetch-depth : 0 # This ensures we check out all tags and branches.
464+ filter : tree:0
463465
464466 - name : install elan
465467 run : |
@@ -530,6 +532,7 @@ jobs:
530532 token : ${{ secrets.MANUAL_PR_BOT }}
531533 ref : nightly-testing
532534 fetch-depth : 0 # This ensures we check out all tags and branches.
535+ filter : tree:0
533536
534537 - name : Check if tag in reference manual exists
535538 if : steps.workflow-info.outputs.pullRequestNumber != '' && steps.reference-manual-ready.outputs.manual_ready == 'true'
0 commit comments