Skip to content

Commit

Permalink
chore: check commit convention in CI (#87)
Browse files Browse the repository at this point in the history
Check the commit convention in CI, as is done in the lean4 repo
  • Loading branch information
david-christiansen authored Oct 21, 2024
1 parent 620fa47 commit 26f932c
Showing 1 changed file with 20 additions and 0 deletions.
20 changes: 20 additions & 0 deletions .github/workflows/pr-title.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
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@v7
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): .*[^.]($|\n\n)/.test(msg)) {
core.setFailed('PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).');
}

0 comments on commit 26f932c

Please sign in to comment.