Check PR title for commit convention

fix: handle dot notation on local variables in grind parameters #33724

Sign in to view logs

Triggered via pull request December 10, 2025 04:10

kim-em

edited #11573

fix-grind-dot-notation-params

Status Failure

Total duration 6s

Artifacts –

pr-title.yml

on: pull_request

Annotations

1 error

check-pr-title

PR title does not follow the Commit Convention (https://leanprover.github.io/lean4/doc/dev/commit_convention.html).