Generate HTML files
yurrriq opened this issue · 3 comments
yurrriq commented
- Do we want these?
- Should we host them on the site too?
- This will require updating
pandoc-minted.hsto support HTML - link them on the site
david-christiansen commented
Why not highlight Idris code using the Idris compiler's notion of highlighting, rather than relying on syntax only?
https://github.com/david-christiansen/idris-code-highlighter is a start for this, though it could be made more friendly!
yurrriq commented
That's a great idea!