From d62268b013b1d03fdafe96c1381c0effbdfd3ad1 Mon Sep 17 00:00:00 2001
From: "Alex J. Best" <alex.j.best@gmail.com>
Date: Sat, 5 Nov 2022 18:46:20 +0100
Subject: [PATCH] better

---
 DocGen4/Output/DocString.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index f9f0e34..f813288 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -188,7 +188,9 @@ 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.find? "class" = "language-lean" then
+    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
       autoLink el
     -- recursively modify
     else