max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: pr-release.yml: fix bot’s username to look for (#5495)

Browse source 
This didn’t make it in with #5490, but seems to be needed, just as in
https://github.com/leanprover-community/mathlib4/pull/17182/files (the
code is duplicated in both repos, and should be the same).
This commit is contained in:
Joachim Breitner 2024-09-27 17:29:53 +02:00 • committed by GitHub
parent e28bfedae2
commit 56b78a0ed1
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.github/workflows/pr-release.yml vendored
View file

@ -167,7 +167,7 @@ jobs:
-H "Authorization: token ${{ secrets.MATHLIB4_COMMENT_BOT }}" \
-H "Accept: application/vnd.github.v3+json" \
"https://api.github.com/repos/leanprover/lean4/issues/${{ steps.workflow-info.outputs.pullRequestNumber }}/comments" \
| jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-mathlib4-bot"))')"
| jq 'first(.[] | select(.body | test("^- . Mathlib") or startswith("Mathlib CI status")) | select(.user.login == "leanprover-community-bot"))')"
existing_comment_id="$(echo "$existing_comment" | jq -r .id)"
existing_comment_body="$(echo "$existing_comment" | jq -r .body)"