diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index b7d7d5f..75966d0 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -108,7 +108,7 @@ def moduleNameToLink (n : Name) : BaseHtmlM String := do Returns the HTML doc-gen4 link to a module name. -/ def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do - pure {module.getString!} + pure {module.toString} /-- Returns the LeanInk link to a module name. diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 9842bba..8d08eaf 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -15,7 +15,7 @@ open scoped DocGen4.Jsx def moduleListFile (file : Name) : BaseHtmlM Html := do pure
- {←moduleToHtmlLink file} + {file.getString!}
/--