fix: fix navbar centering
parent
28bb2abe40
commit
a5dfba5f1c
|
@ -14,7 +14,7 @@ open Lean
|
||||||
open scoped DocGen4.Jsx
|
open scoped DocGen4.Jsx
|
||||||
|
|
||||||
def moduleListFile (file : Name) : HtmlM Html := do
|
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>
|
<a href={← moduleNameToLink file}>{file.toString}</a>
|
||||||
</div>
|
</div>
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue