r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

fix: intersperse code contents

main
Xubai Wang 2022-02-18 04:01:31 +08:00
parent 5dc3ab855f
commit cce4285c96
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
DocGen4/Output/DocString.lean
View File

@ -103,7 +103,7 @@ partial def modifyElement (element : Element) (linkCode : Bool := true) : HtmlM
for c in contents do for c in contents do
match c with match c with
| Content.Character s => | Content.Character s =>
newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor) newContents := newContents ++ (← s.splitOn.mapM possibleNameToAnchor).intersperse (Content.Character " ")
| _ => newContents := newContents.push c | _ => newContents := newContents.push c
pure ⟨ name, attrs, newContents⟩ pure ⟨ name, attrs, newContents⟩
-- recursively modify -- recursively modify