Closed yomimono closed 6 years ago
Thanks very much, @dbuenzli !
You are welcome. Note there are still a lot of these {1:top ...}
heading that will generate incorrect markup (they translate to #top
html fragments identifiers which need to be unique in a document).
In general it's better to put {1:id
yourself everywhere for linkability. IIRC I think nowadays odoc
generate ones automatically for you but they are based on the header content (à la markdown) which is always a bit more brittle.
Thanks a lot! This is starting to look like a piece of software someone might actually use, rather than a panicked code-dump.
Comments and suggestions are extremely welcome.