feat: make release notes insert parts from markdown - #599

Merged

jcreedcmu merged 9 commits into

leanprover:nightly-testingfrom

jcreedcmu:release-notes

Oct 9, 2025

Commits on Oct 8, 2025

feat: make release notes insert parts from markdown
jcreedcmu
committed
52854f0
Fix unbounded markdown header level growth
jcreedcmu
committed
cab1591
Fix a couple of redundant sections
jcreedcmu
committed
111ccc5
Revert "Fix a couple of redundant sections"
jcreedcmu
committed
edf0d0a
Adapt to leanprover/verso#539
jcreedcmu
committed
9044611
Make matching against markdown part command more general
jcreedcmu
committed
4542576
Adapt to https://github.com/leanprover/verso/pull/539
jcreedcmu
committed
5e8f3d8
Refactor section closing slightly
jcreedcmu
committed
cb51896

Commits on Oct 9, 2025

Exclude release notes from vale checking
jcreedcmu
committed
1dfc0db