diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index 2238cc3..f9f0e34 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -188,7 +188,7 @@ partial def modifyElement (element : Element) : HtmlM Element := else if name = "a" then extendAnchor el -- auto link for inline - else if name = "code" ∧ attrs.contains "language-lean" then + else if name = "code" ∧ attrs.find? "class" = "language-lean" then autoLink el -- recursively modify else