Merge branch 'main' into chore/pin-3rd-party-actions

Author: tjaniczek

.github/workflows/check-repro.yml

@@ -10,7 +10,7 @@ jobs:
     if: ${{ github.event.label.name == 'bug' }}
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7
+      - uses: actions/github-script@60a0d83039c74a4aee543508d2ffcb1c3799cdea # v7.0. 
         with:
           github-token: ${{ secrets.GITHUB_TOKEN }}
           script: |