bot fix style #96365
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: bot fix style | |
| # triggers the action when | |
| on: | |
| issue_comment: | |
| # the PR receives a comment, or a comment is edited | |
| types: [created, edited] | |
| pull_request_review: | |
| # triggers on a review, whether or not it is accompanied by a comment | |
| types: [submitted] | |
| pull_request_review_comment: | |
| # triggers on a review comment | |
| types: [created, edited] | |
| jobs: | |
| fix_style: | |
| # we set some variables. The ones of the form `${{ X }}${{ Y }}` are typically not | |
| # both set simultaneously: depending on the event that triggers the PR, usually only one is set | |
| env: | |
| AUTHOR: ${{ github.event.comment.user.login }}${{ github.event.review.user.login }} | |
| COMMENT_EVENT: ${{ github.event.comment.body }} | |
| COMMENT_REVIEW: ${{ github.event.review.body }} | |
| COMMENT_REVIEW_COMMENT: ${{ github.event.pull_request_review_comment.body }} | |
| name: Fix style issues from lint | |
| # the `if` works with `comment`s, but not with `review`s or `review_comment`s | |
| # if: github.event.issue.pull_request | |
| # && (startsWith(github.event.comment.body, 'bot fix style') || contains(toJSON(github.event.comment.body), '\nbot fix style')) | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: leanprover-community/lint-style-action@a7e7428fa44f9635d6eb8e01919d16fd498d387a # 2025-08-18 | |
| with: | |
| mode: fix | |
| lint-bib-file: true | |
| BOT_FIX_STYLE_TOKEN: ${{ secrets.GITHUB_TOKEN }} |