From 96147eaa0c066a95210fe5518c987e77be034b9f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Mon, 13 Nov 2023 23:13:58 +0100
Subject: [PATCH] feat: type doc right below initial type naming

---
 DocGen4/Output/Module.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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]
       </div>
     </div>