chore(.github/workflows): don't rely on linkifier in maintainer merge…

… messages (#19046) Not tested, and I'm just guessing that the relevant properties exist as I can't find the relevant API docs... Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Eric Wieser <[email protected]>
leanprover-community · May 19, 2023 · ef7403f · ef7403f
1 parent a7c017d
commit ef7403f
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/.github/workflows/maintainer_merge_comment.yml b/.github/workflows/maintainer_merge_comment.yml
@@ -30,7 +30,7 @@ jobs:
           type: 'stream'
           topic: 'maintainer merge'
           content: |
-            ${{ format('{0} requested a maintainer merge on PR #{1}:', github.event.comment.user.login, github.event.issue.number) }}
+            ${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.comment.user.login, github.event.issue.number, github.event.issue.html_url) }}
 
             > ${{ github.event.issue.title }}
 

diff --git a/.github/workflows/maintainer_merge_review.yml b/.github/workflows/maintainer_merge_review.yml
@@ -28,7 +28,7 @@ jobs:
           type: 'stream'
           topic: 'maintainer merge'
           content: |
-            ${{ format('{0} requested a maintainer merge on PR #{1}:', github.event.review.user.login, github.event.pull_request.number) }}
+            ${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.review.user.login, github.event.pull_request.number, github.event.pull_request.html_url) }}
 
             > ${{ github.event.pull_request.title }}
 

diff --git a/.github/workflows/maintainer_merge_review_comment.yml b/.github/workflows/maintainer_merge_review_comment.yml
@@ -28,7 +28,7 @@ jobs:
           type: 'stream'
           topic: 'maintainer merge'
           content: |
-            ${{ format('{0} requested a maintainer merge on PR #{1}:', github.event.comment.user.login, github.event.pull_request.number) }}
+            ${{ format('{0} requested a maintainer merge on PR [#{1}]({2}):', github.event.comment.user.login, github.event.pull_request.number, github.event.pull_request.html_url) }}
 
             > ${{ github.event.pull_request.title }}