diff --git a/.github/workflows/pr-title.yml b/.github/workflows/pr-title.yml index dcb5dd5f8718..40556c5c7bcc 100644 --- a/.github/workflows/pr-title.yml +++ b/.github/workflows/pr-title.yml @@ -1,8 +1,9 @@ name: Check PR title for commit convention on: + merge_group: pull_request: - types: [opened, edited] + types: [opened, synchronize, reopened, edited] jobs: check-pr-title: @@ -12,6 +13,8 @@ jobs: uses: actions/github-script@v6 with: script: | - if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(context.payload.pull_request.title)) { + const msg = context.payload.pull_request? context.payload.pull_request.title : context.payload.merge_group.head_commit.message; + console.log(`Message: ${msg}`) + if (!/^(feat|fix|doc|style|refactor|test|chore|perf): .*[^.]($|\n\n)/.test(msg)) { core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).'); }