Literate forester without external tool #8290
Conversation
1. one line somehow failed when using --html-highlight=code
2. but in this new setup using --html without --html-highlight=code
won't provide valid html
but enforce \agda{...} block have to write in a readable way is not a
bad thing, so I decide to remove the test case for now (because I have
no idea how to fix it for now)
1. reorder command (I found forester assets is a bit changed? Old way didn't work anyway) 2. Mention the problem of links and how to fix self-link 3. To my best, external link has no universal solution, hence I only point it out here
707d974 to
f506fb9
Compare
andreasabel
left a comment
There was a problem hiding this comment.
Thanks for the PR.
Eventually, this will need a CHANGELOG entry as well.
It would be good if the testsuite contained a full example, including a forest.toml, so that only a few steps are needed to get some rendered example.
(I tried but forester build only produces .xml files and my browser displays just an empty page if I open them.)
Got it.
Ok, in Build steps
Run serve
Run serve |
resolve #8281
(Andreas:) doc rendered at https://agda--8290.org.readthedocs.build/en/8290/tools/literate-programming.html#literate-forester