fix: regression in import names

main
Henrik Böving 2023-01-01 18:59:19 +01:00
parent bdf803b100
commit a5caefc03f
2 changed files with 2 additions and 2 deletions

View File

@ -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.

View File

@ -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>
/--