In the docstring of `Html.text` in `src/verso/Verso/Output/Html.lean`: ``` If `escape` is `true`, then characters such as `'&'` are escaped to entities such as `"&"` during rendering. ``` At https://verso.lean-lang.org/doc/latest/Output-Formats/#Verso___Output___Html___text, the `"&"` is appears as `"&"`. Expected: `"&"`.
In the docstring of
Html.textinsrc/verso/Verso/Output/Html.lean:At https://verso.lean-lang.org/doc/latest/Output-Formats/#Verso___Output___Html___text, the
"&"is appears as"&". Expected:"&".