lean4-htt/.github
Joachim Breitner 56b78a0ed1
chore: pr-release.yml: fix bot’s username to look for (#5495)
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).
2024-09-27 15:29:53 +00:00
..
ISSUE_TEMPLATE
workflows chore: pr-release.yml: fix bot’s username to look for (#5495) 2024-09-27 15:29:53 +00:00
PULL_REQUEST_TEMPLATE.md