From a18b27f4c1c4526a3c3b3f958f0e23a05a34aadb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 1 Jan 2023 20:00:42 +0100 Subject: [PATCH] feat: attempt to improve usability of the file tree --- DocGen4/Output/Navbar.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index c6de80d..4280864 100644 --- 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 - {← moduleToHtmlLink h.getName} + {s!"{h.getName.getString!} ({file})"} else {h.getName.getString!}