fix: typo in script (#1009)

leanprover-community · Oct 27, 2024 · 75fb097 · 75fb097
1 parent cbe41b9
commit 75fb097
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml
@@ -18,8 +18,8 @@ jobs:
       - name: Get PR info
         id: pr-info
         run: |
-          echo "pullRequestNumber=$(gh pr --json number -q .number || echo '')" >> $GITHUB_OUTPUTS
-          echo "targetBranch=$(gh pr --json baseRefName -q .baseRefName || echo '')" >> $GITHUB_OUTPUTS
+          echo "pullRequestNumber=$(gh pr view --json number -q .number || echo '')" >> $GITHUB_OUTPUTS
+          echo "targetBranch=$(gh pr view --json baseRefName -q .baseRefName || echo '')" >> $GITHUB_OUTPUTS
 
       - name: Checkout mathlib4 repository
         if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'