diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 97414d5..e7ec326 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -81,7 +81,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i) | _ => nodes := nodes - nodes := nodes.push : + nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"] nodes := nodes.push
[←infoFormatToHtml doc.getType]
pure
[nodes]
diff --git a/lakefile.lean b/lakefile.lean index 8d172dc..e73161f 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -114,4 +114,4 @@ library_facet docs (lib) : FilePath := do let traces ← staticFiles.mapM computeTrace let indexTrace := mixTraceArray traces - return (dataFile, trace.mix indexTrace) + return (dataFile, trace.mix indexTrace) \ No newline at end of file