James Wood (Nov 14 2022 at 15:43): James Wood (Nov 14 2022 at 15:43):I want to add a little bit of CSS (below) to my coqdoc HTML output. What's the best way to do this in a way compatible with coq_makefile (i.e, in a way that won't be clobbered when I or others run make html)?
#main .doc pre { line-height: 16px; }
you might want to use the --with-header option like here
James Wood (Nov 15 2022 at 09:54):Thanks, looks like a good starting point.
James Wood (Nov 15 2022 at 10:09):Is the --with-header option documented anywhere?
Karl Palmskog (Nov 15 2022 at 10:10):coqdoc --help
James Wood (Nov 15 2022 at 10:18):One line with a typo :neutral:. I'm confused, though, because you can't just concatenate things onto an HTML file and expect a reasonable result.
James Wood (Nov 15 2022 at 10:20):I guess coqdoc has a default value for --with-header, and I have to copy a lot of that to add the bit I want.
Paolo Giarrusso (Nov 16 2022 at 00:35):https://github.com/coq-community/coqdocjs has a concrete example. Concatenation works because header and footer aren't complete HTMLs
Last updated: Sep 30 2023 at 06:01 UTC