lean4-htt/doc/dev
Kim Morrison 42a0e92453
doc: clarify release notes timing with reference-manual tags (#12171)
This PR documents an issue encountered during the v4.28.0-rc1 release:
if release notes are merged to the reference-manual repository AFTER the
version tag is created, the deployed documentation won't include them.

The fix is to either:
1. Include release notes in the same PR as the toolchain bump (or merge
before tagging)
2. Regenerate the tag after merging release notes

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.5 <noreply@anthropic.com>
2026-01-27 06:12:59 +00:00
..
bootstrap.md doc: clarify how to trigger automatic stage0 updates (#11413) 2025-11-28 12:56:59 +00:00
commit_convention.md doc: commit conventions and Mathlib CI (#6605) 2025-01-13 02:29:46 +00:00
debugging.md doc: stderrAsMessages is now the default on the cmdline as well (#4955) 2024-08-08 10:28:22 +00:00
ffi.md doc: replace ffi.md with links to the reference manual (#11737) 2025-12-19 07:23:06 +00:00
index.md doc: testing Lean while avoiding rebuilds for downstream projects (#10328) 2025-09-10 13:53:34 +00:00
release_checklist.md doc: clarify release notes timing with reference-manual tags (#12171) 2026-01-27 06:12:59 +00:00
testing.md doc: note that tests/lean/run disables linters (#11595) 2025-12-11 01:33:07 +00:00