Christian Doczkal (Sep 03 2020 at 09:44): Christian Doczkal (Sep 03 2020 at 09:44):I have a large development consisting of several parts, each in their own directory, that is built centrally using one Makefile generated from a central _CoqProject. Unfortunately, this generates a very long table of contents. In order to make this a little more structured, I'm currently patching toc.html, breaking up the long unordered list by inserting:
</ul>
<h2> Part Foo </h2>
<ul>
in between the parts coming from the individual directories. Is there a less hacky/more maintainable way to do this? This is not to be confused with dropping the --short option, which would yield a (non-customizable) header for each and every file.
Last updated: Apr 20 2024 at 04:02 UTC