Customise doc-gen4 home page

Stream: general

[Joseph Tooby-Smith]

I am using doc-gen4 on my project. The way I have it currently set up is to generate, via a workflow, the docs on a push to the main branch.

I would like to customise the home-page (the page which defaults to saying This was built using Lean 4 at commit ....) to include some basic mark-down text about the project. Does anyone know of an easy way of doing this, besides forking doc-gen4 and manually editing?

[Henrik Böving]

This issue is tracked here https://github.com/leanprover/doc-gen4/issues/43. Someone can implement what xubai suggested there if they want to.

[Jz Pan]

Marked. There is also a a hard-coded one https://github.com/leanprover/doc-gen4/pull/172