Skip to content

ci: allow ci prefix in PR titles - #355

Merged
fmontesi merged 1 commit into
leanprover:mainfrom
chenson2018:ci-title
Feb 19, 2026
Merged

ci: allow ci prefix in PR titles#355
fmontesi merged 1 commit into
leanprover:mainfrom
chenson2018:ci-title

ci: allow ci prefix in PR titles

1ce9653
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

The logs for this run have expired and are no longer available.