doc-gen4 icon indicating copy to clipboard operation
doc-gen4 copied to clipboard

Populate the index page

Open xubaiw opened this issue 3 years ago • 0 comments

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).

截屏2022-02-25 下午12 12 33

xubaiw avatar Feb 25 '22 04:02 xubaiw