Skip to content

Commit ac0e252

Browse files
fix: get author of pull request for PR review / PR review comment (#21278)
[Zulip thread (in reviewers stream)](https://leanprover.zulipchat.com/#narrow/channel/345428-mathlib-reviewers/topic/add.20author.20to.20.60maintainer-merge.60.20Zulip.20message)
1 parent e4f90bc commit ac0e252

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

.github/workflows/maintainer_merge.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ jobs:
1919
# both set simultaneously: depending on the event that triggers the PR, usually only one is set
2020
env:
2121
AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }}
22-
PR_AUTHOR: ${{ github.event.issue.user.login }}
22+
PR_AUTHOR: ${{ github.event.issue.user.login }}${{ github.event.pull_request.user.login }}
2323
PR_NUMBER: ${{ github.event.issue.number }}${{ github.event.pull_request.number }}
2424
COMMENT_EVENT: ${{ github.event.comment.body }}
2525
COMMENT_REVIEW: ${{ github.event.review.body }}

0 commit comments

Comments
 (0)