diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 75966d0..b7d7d5f 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.toString}
+ pure {module.getString!}
/--
Returns the LeanInk link to a module name.
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index f5d2612..fb5fbe3 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -33,7 +33,7 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
if h.isFile then
{←moduleToHtmlLink h.getName}
else
- {h.getName.toString}
+ {h.getName.getString!}
pure