doc-gen4
doc-gen4 copied to clipboard
Populate the index page
Users may want to have customized content in their index page.
A simple solution is to add a Cli FLAG
that allows users to specify a .html
or .md
file.
The more comprehensive method is to have a configuration file similar to lakefile.lean
, so that people can customize everything from documentation title to additional navbar pages (like that of mathlib).
