c41cb64ca7
This PR updates the `pr-title` CI check to enforce that the commit message does not start with a capital letter followed by a non-capital letter. This should ensure that messages do not start with a capitalized word, but allow messages that start with an acronym.
20 lines
750 B
YAML
20 lines
750 B
YAML
name: Check PR title for commit convention
|
|
|
|
on:
|
|
merge_group:
|
|
pull_request:
|
|
types: [opened, synchronize, reopened, edited]
|
|
|
|
jobs:
|
|
check-pr-title:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- name: Check PR title
|
|
uses: actions/github-script@v8
|
|
with:
|
|
script: |
|
|
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): (?![A-Z][a-z]).*[^.]($|\n\n)/.test(msg)) {
|
|
core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
|
|
}
|