Lars Eggert 6dd295b1a5 Insert nav subheadings in the right place. (#4967) ... * Insert nav subheadings in the right place. Fixes #4924 * Undo erroneous commit		2023-01-12 12:23:11 -06:00
..
css	More fixes for HTMLization and PDFization (#4899)	2022-12-19 09:04:44 -06:00
images	feat: better htmlization views (#4825)	2022-12-02 15:17:14 -06:00
js	Insert nav subheadings in the right place. (#4967)	2023-01-12 12:23:11 -06:00
.gitignore	More fixes	2021-12-08 08:55:45 +00:00