From a5caefc03feb997a94ed9ad7ee30e0393f279818 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 1 Jan 2023 18:59:19 +0100
Subject: [PATCH] fix: regression in import names

---
 DocGen4/Output/Base.lean   | 2 +-
 DocGen4/Output/Navbar.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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 <a href={←moduleNameToLink module}>{module.getString!}</a>
+  pure <a href={←moduleNameToLink module}>{module.toString}</a>
 
 /--
 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 <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
-    {←moduleToHtmlLink file}
+    <a href={←moduleNameToLink file}>{file.getString!}</a>
   </div>
 
 /--