From 5b4d779b31db05a72d649d802a4a1563a9a17121 Mon Sep 17 00:00:00 2001 From: Alex J Best Date: Mon, 16 Oct 2023 17:29:39 +0100 Subject: [PATCH] Update DocGen4/Output/DocString.lean --- DocGen4/Output/DocString.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 71c4cdb..4f5a7dd 100644 --- 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