From 75fb097c5dec0fb3951322dec96602eb2cc34581 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= <fgdorais@gmail.com>
Date: Sun, 27 Oct 2024 19:54:27 -0400
Subject: [PATCH] fix: typo in script (#1009)

---
 .github/workflows/test_mathlib.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/test_mathlib.yml b/.github/workflows/test_mathlib.yml
index c3904f3227..6b5c7a4d94 100644
--- 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'