doc: Add changelog to users guide. #708
Conversation
doc/UsersGuide/Releases/v4_27_0.lean
Outdated
|
|
||
| import VersoManual | ||
|
|
||
| -- EJGA: Should we use the markdown code block from ref-manual? |
There was a problem hiding this comment.
I think not. That exists as an artifact of the "export from GitHub" feature. We can just write them in Verso.
There was a problem hiding this comment.
Thanks! Updated to:
* Add Release Notes / Changelog to Verso Users guide (@ejgallego, #708)
Would that work OK? I'd be happy to implement a PR role, so we could instead do {pr 708}.
There was a problem hiding this comment.
I think {pr}[708] would be nice, but we don't need it. If you feel like it, go for it, but better to get the rest of your dependent PRs merged.
There was a problem hiding this comment.
Makes sense, thanks. I'll do the {pr ...} role in a separate, low-prio PR.
| htmlSplit := .never | ||
| %%% | ||
|
|
||
| This section provides release notes about recent versions of Verso. When updating to a new version, please |
There was a problem hiding this comment.
I think we should have a little note here that our version numbers are synced with the Lean version, so there's one Verso release per Lean release with no expectation of cross-Lean-version compatibility. In other words, our version number in this manual is not a semantic version.
There was a problem hiding this comment.
Thanks for the comments. Should be addressed.
ejgallego
changed the title
Co-authored-by: David Thrane Christiansen <[email protected]>
2 participants
No description provided.