From 108d36d0f094c7e5f281109cb78fe0cd7193dbc2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 27 Jul 2022 14:19:40 +0200
Subject: [PATCH] fix: whitespace after declaration without arguments

Closes: #76
---
 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 97414d5..e7ec326 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -81,7 +81,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i)
   | _ => nodes := nodes
 
-  nodes := nodes.push <span class="decl_args">:</span>
+  nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"]
   nodes := nodes.push <div class="decl_type">[←infoFormatToHtml doc.getType]</div>
   pure <div class="decl_header"> [nodes] </div>