feat: attempt to improve usability of the file tree

2023-01-01 20:00:42 +01:00 · 2023-01-01 20:00:42 +01:00 · a18b27f4c1
parent d5ef8006b7
commit a18b27f4c1
1 changed files with 1 additions and 1 deletions
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@ -31,7 +31,7 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
  let moduleLink ← moduleNameToLink h.getName
  let summary :=
    if h.isFile then
-      <summary>{← moduleToHtmlLink h.getName}</summary>
+      <summary>{s!"{h.getName.getString!} ({<a href={← moduleNameToLink h.getName}>file</a>})"} </summary>
    else
      <summary>{h.getName.getString!}</summary>