verso icon indicating copy to clipboard operation
verso copied to clipboard
verified publisher icon leanprover

feat: convert docComments in Literate Lean pages

Open pimotte opened this issue 8 months ago • 0 comments

This feature is controlled by the verso.literateMarkdown.convertDoccomments option, which defaults to false for backwards compatibility.

pimotte avatar Jun 09 '25 16:06 pimotte