From 3d84e61917b2cfdbe59131d32ad76edd38e0e3bf Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 27 Oct 2024 21:01:42 -0400
Subject: [PATCH] fix: github script fix repo

---
 .github/workflows/test_mathlib.yml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml
index c367804aa3..3a6ece425e 100644
--- a/.github/workflows/test_mathlib.yml
+++ b/.github/workflows/test_mathlib.yml
@@ -14,12 +14,19 @@ jobs:
     steps:
       - name: Checkout PR
         uses: actions/checkout@v4
+        with:
+          repository: ${{ github.event.workflow_run.head_repository }}
+          ref: ${{github.event.workflow_run.head_branch }}
+          fetch-depth: 0
 
       - name: Get PR info
         id: pr-info
         run: |
           echo "pullRequestNumber=$(gh pr view --json number -q .number || echo '')" >> $GITHUB_OUTPUT
           echo "targetBranch=$(gh pr view --json baseRefName -q .baseRefName || echo '')" >> $GITHUB_OUTPUT
+          echo "HEAD_BRANCH=$(gh pr view --json headRefName -q .headRefName || echo '')" >> $GITHUB_ENV
+          echo "HEAD_REPO=$(gh pr view --json headRepository -q .headRepository.name || echo '')" >> $GITHUB_ENV
+          echo "HEAD_OWNER=$(gh pr view --json headRepositoryOwner-q .headRepositoryOwner.login || echo '')" >> $GITHUB_ENV
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
 
@@ -45,13 +52,14 @@ jobs:
         id: check_mathlib_tag
         env:
           PR_NUMBER: ${{ steps.pr-info.outputs.pullRequestNumber }}
+          HEAD_OWNER: ${{ env.HEAD_OWNER }}
           HEAD_REPO: ${{ env.HEAD_REPO }}
           HEAD_BRANCH: ${{ env.HEAD_BRANCH }}
         run: |
           git config user.name "leanprover-community-mathlib4-bot"
           git config user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
 
-          echo "PR info: $HEAD_REPO $HEAD_BRANCH"
+          echo "PR info: $HEAD_OWNER $HEAD_REPO $HEAD_BRANCH"
 
           BASE=master
           echo "Using base tag: $BASE"