doc-gen icon indicating copy to clipboard operation
doc-gen copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Switch to using markdownit for rendering

Open eric-wieser opened this issue 1 year ago • 0 comments

This doesn't actually work yet, but contains enough to debug the renderer on the latex.md file

Blocked by https://github.com/executablebooks/mdit-py-plugins/pull/46

eric-wieser avatar Mar 03 '23 20:03 eric-wieser