From 07cb0ed1ccffa99136afb8caead78c7b6cc1b1a0 Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Sat, 5 Nov 2022 18:28:27 +0100
Subject: [PATCH] fix

---
 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 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 <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