From 6ffa7f94fd001ac92dc4985eb02d4848f12f7431 Mon Sep 17 00:00:00 2001
From: Joshua Potter <jrpotter2112@gmail.com>
Date: Wed, 8 Nov 2023 01:08:55 -0700
Subject: [PATCH] Fix `docStringToHtml`.

---
 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 c39c4c8..ca4cdb9 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -210,7 +210,7 @@ partial def modifyElement (element : Element) : HtmlM Element :=
 
 /-- Convert docstring to Html. -/
 def docStringToHtml (s : String) : HtmlM (Array Html) := do
-    let rendered := CMark.renderHtml (Html.escape s)
+  let rendered := CMark.renderHtml (Html.escape s)
   match manyDocument rendered.mkIterator with
   | Parsec.ParseResult.success _ res =>
     res.mapM fun x => do return Html.text <| toString (← modifyElement x)