From 95b79c1744708f33a8dd3adaaa3af759a96dd59a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 22 Jul 2022 17:03:24 +0200 Subject: [PATCH] fix: Fix linking of importedBy modules --- DocGen4/Output.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 2a596ed..db1d156 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -132,7 +132,7 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do let fileContent ← FS.readFile entry.path let .ok jsonContent := Json.parse fileContent | unreachable! let .ok (module : JsonModule) := fromJson? jsonContent | unreachable! - allModules := (module.name, Json.str <| moduleNameToLink module.name |>.run baseConfig) :: allModules + allModules := (module.name, Json.str <| moduleNameToLink (String.toName module.name) |>.run baseConfig) :: allModules allDecls := (module.declarations.map (λ d => (d.name, toJson d))) ++ allDecls for inst in module.instances do let mut insts := allInstances.findD inst.className #[]