bf269ce250
This PR fixes a bug where the nesting level in Verso Docstrings is forgotten when there's a doc comment with no headers. It changes the `terminalNesting` of `VersoModuleDocs` to be recomputed rather than stored in the structure; we never want it to be anything besides the default value, and it's easy to accidentally break this invariant. Closes #13485
13 lines
65 B
Text
13 lines
65 B
Text
set_option doc.verso true
|
|
|
|
/-!
|
|
# A
|
|
|
|
## B
|
|
-/
|
|
|
|
/-! -/
|
|
|
|
/-!
|
|
## C
|
|
-/
|