Update DocGen4/Output/DocString.lean

leanprover · Oct 16, 2023 · 5b4d779 · 5b4d779
1 parent 074c783
commit 5b4d779
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
@@ -214,7 +214,7 @@ def docStringToHtml (s : String) : HtmlM (Array Html) := do
   match manyDocument rendered.mkIterator with
   | Parsec.ParseResult.success _ res =>
     res.mapM fun x => do return Html.text <| toString (← modifyElement x)
-  | _ => return #[Html.text <| rendered]
+  | _ => return #[Html.text rendered]
 
 end Output
 end DocGen4