From fc00a41ecb606b9ebde7eeca1d626c4914fba034 Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Sun, 6 Nov 2022 21:27:26 +0100
Subject: [PATCH] bool

---
 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 f813288..e59f287 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -190,7 +190,7 @@ partial def modifyElement (element : Element) : HtmlM Element :=
     -- auto link for inline <code></code>
     else if name = "code" ∧
       -- don't linkify code blocks explicitly tagged with a language other than lean
-      ((¬ attrs.contains "class") ∨ (((attrs.find? "class").getD "").splitOn).filter (fun s => s.startsWith "language-" ∧ s ≠ "language-lean") = []) then
+      (((attrs.find? "class").getD "").splitOn.all (fun s => s == "language-lean" || !s.startsWith "language-")) then
       autoLink el
     -- recursively modify
     else