Properly get PR number for merge group (#1077)

Run
https://github.com/mmtk/mmtk-core/actions/runs/7649653943/job/20844445119
failed, as we use `${{ github.event.pull_request.number }}` to get the
pull request number and it does not work for the `merge_group` trigger.
This PR gets pull request number using a third-party action which
properly deals with both `pull_request` and `merge_group`.

Author: qinsoon

.github/workflows/minimal-tests-bindings.yml

@@ -18,15 +18,26 @@ jobs:
   # This step allows 2mins before we check comments for binding repos/refs.
   grace-period:
     runs-on: ubuntu-latest
+    outputs:
+      pr-number: ${{ steps.set-output.outputs.pr-number }}
     steps:
+      # This workflow runs for both merge_group and pull_request
+      # We need a way to get the pull request number that works for both cases.
+      # The action can do that.
+      - id: get-pr-number
+        uses: mgaitan/gha-get-pr-number@main
+      # This job also outputs the PR number
+      - id: set-output
+        run: echo "pr-number=${{ steps.get-pr-number.outputs.number }}" >> $GITHUB_OUTPUT
+      # Sleep for 2 mins
       - run: sleep 120
 
   # Figure out binding PRs.
   binding-refs:
     needs: grace-period
     uses: ./.github/workflows/pr-binding-refs.yml
     with:
-      pull_request: ${{ github.event.pull_request.number }}
+      pull_request: ${{ needs.grace-period.outputs.pr-number }}
 
   minimal-tests-openjdk:
     needs: binding-refs