From a5dfba5f1ccc840a0946f7bd23d3c6bf8e133068 Mon Sep 17 00:00:00 2001
From: Xubai Wang <self@xubai.wang>
Date: Wed, 23 Feb 2022 23:09:10 +0800
Subject: [PATCH] fix: fix navbar centering

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

diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index efc9735..e56aa38 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -14,7 +14,7 @@ open Lean
 open scoped DocGen4.Jsx
 
 def moduleListFile (file : Name) : HtmlM Html := do
-  pure <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+  pure <div «class»={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
     <a href={← moduleNameToLink file}>{file.toString}</a>
   </div>