Skip to content

Commit

Permalink
fix: missing github token
Browse files Browse the repository at this point in the history
  • Loading branch information
fgdorais committed Oct 28, 2024
1 parent 75fb097 commit 63cfd3c
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/test_mathlib.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@ jobs:
run: |
echo "pullRequestNumber=$(gh pr view --json number -q .number || echo '')" >> $GITHUB_OUTPUTS
echo "targetBranch=$(gh pr view --json baseRefName -q .baseRefName || echo '')" >> $GITHUB_OUTPUTS
env:
GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}

- name: Checkout mathlib4 repository
if: steps.pr-info.outputs.pullRequestNumber != '' && steps.pr-info.outputs.targetBranch == 'main'
Expand Down

0 comments on commit 63cfd3c

Please sign in to comment.