From cce4285c96349ebab7dcffe95ba9f4631bb00f9c Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 04:01:31 +0800 Subject: [PATCH] fix: intersperse code contents --- 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 70e6b0d..d318752 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -103,7 +103,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM for c in contents do match c with | Content.Character s => - newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor) + newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor).intersperse (Content.Character " ") | _ => newContents := newContents.push c pure ⟨ name, attrs, newContents⟩ -- recursively modify