fix

2022-11-05 18:28:27 +01:00 · 2022-11-05 18:28:27 +01:00 · 07cb0ed1cc
parent 58fcc5d468
commit 07cb0ed1cc
1 changed files with 1 additions and 1 deletions
--- 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 <code></code>
-    else if name = "code" ∧ attrs.contains "language-lean" then
+    else if name = "code" ∧ attrs.find? "class" = "language-lean" then
      autoLink el
    -- recursively modify
    else