r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: type doc right below initial type naming

main
Henrik Böving 2023-11-13 23:13:58 +01:00
parent d70c8b78f8
commit 96147eaa0c
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Output/Module.lean
View File

@ -133,8 +133,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
[leanInkHtml] [leanInkHtml]
[attrsHtml] [attrsHtml]
{← docInfoHeader doc} {← docInfoHeader doc}
[docInfoHtml]
[docStringHtml] [docStringHtml]
[docInfoHtml]
[extraInfoHtml] [extraInfoHtml]
</div> </div>
</div> </div>