Merge branch 'main' into main

This commit is contained in:
Joseph Julicher 2023-09-27 18:19:10 -07:00 committed by GitHub
commit b71a5573f7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -13,9 +13,9 @@ env:
jobs: jobs:
Formatting: Formatting:
name: Run Formatting Check name: Run Formatting Check
if: ${{ github.event.issue.pull_request }} && if: ${{ github.event.issue.pull_request &&
( ( github.event.comment.body == '/bot run uncrustify' ) || ( ( github.event.comment.body == '/bot run uncrustify' ) ||
( github.event.comment.body == '/bot run formatting' ) ) ( github.event.comment.body == '/bot run formatting' ) ) }}
runs-on: ubuntu-20.04 runs-on: ubuntu-20.04
steps: steps:
- name: Apply Formatting Fix - name: Apply Formatting Fix