Put field docstrings after the field

2023-08-18 08:38:59 +01:00 · 2023-08-18 08:38:59 +01:00 · e5ff71991d
parent 596782c1fe
commit e5ff71991d
1 changed files with 1 additions and 1 deletions
--- 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