From d3d67c1d927663e64d40c1bf6413ece72a2ba9a5 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 18 Aug 2023 08:40:27 +0100
Subject: [PATCH] Do the same for inductives

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

diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 0afeaf6..fde7d40 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -22,8 +22,8 @@ def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
     let renderedDoc ← docStringToHtml doc
     pure
       <li class="constructor" id={name}>
-        <div class="inductive_ctor_doc">[renderedDoc]</div>
         {shortName} : [← infoFormatToHtml c.type]
+        <div class="inductive_ctor_doc">[renderedDoc]</div>
       </li>
   else
     pure