Commit graph

2 commits

Author SHA1 Message Date
Kim Morrison
da55b2e19b
chore: updates to release_checklist.md (#7817)
This PR updates `release_checklist.md`, reflecting current practice and
automation.
2025-04-04 03:45:36 +00:00
Kyle Miller
d984030c6a
chore: set up procedure for preparing release notes (#4247)
We are switching to a new system for preparing release notes.
* Release notes will be compiled when creating a release candidate from
all the commits that are part of that release.
* PRs can include suggestions for release notes in PR messages. Please
use language such as "release notes" and "breaking changes" to call
attention to the suggestions. Release notes are user-centric rather than
developer-centric.
* For more complicated release notes, these can be put into the
`releases_drafts` folder.

This solves an issue where PRs that include release notes can, when
merged, have those notes appear under the wrong Lean version, since they
might have been created before a release but not merged until after. It
also solves merge conflicts due to multiple PRs updating the release
notes.
2024-05-23 02:46:11 +00:00