doc-gen4
                                
                                 doc-gen4 copied to clipboard
                                
                                    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).
