Update DocGen4/Output/DocString.lean

main
Alex J Best 2023-10-16 17:29:39 +01:00 committed by Henrik Böving
parent 074c783259
commit 5b4d779b31
1 changed files with 1 additions and 1 deletions

View File

@ -214,7 +214,7 @@ def docStringToHtml (s : String) : HtmlM (Array Html) := do
match manyDocument rendered.mkIterator with match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res => | Parsec.ParseResult.success _ res =>
res.mapM fun x => do return Html.text <| toString (← modifyElement x) res.mapM fun x => do return Html.text <| toString (← modifyElement x)
| _ => return #[Html.text <| rendered] | _ => return #[Html.text rendered]
end Output end Output
end DocGen4 end DocGen4