diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index b14b6da..df6ac05 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -133,8 +133,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do [leanInkHtml] [attrsHtml] {← docInfoHeader doc} - [docInfoHtml] [docStringHtml] + [docInfoHtml] [extraInfoHtml]