From e5ff71991d8102b9711211a6d8e8880534100e41 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 18 Aug 2023 08:38:59 +0100
Subject: [PATCH] Put field docstrings after the field

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

diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index f4ab138..8f48dc3 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -18,8 +18,8 @@ def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
     let renderedDoc ← docStringToHtml doc
     pure
       <li id={name} class="structure_field">
-        <div class="structure_field_doc">[renderedDoc]</div>
         <div class="structure_field_info">{s!"{shortName} "} : [← infoFormatToHtml f.type]</div>
+        <div class="structure_field_doc">[renderedDoc]</div>
       </li>
   else
     pure