From e02f229305b3450cc119692109a44d46217c180b Mon Sep 17 00:00:00 2001
From: Alok Singh <alokbeniwal@gmail.com>
Date: Mon, 15 Dec 2025 06:29:11 -0800
Subject: [PATCH] chore: fix typo "Unkown" -> "Unknown" in role error message
 (#11682)

Fix a typo in the error message when an unknown role is used in a
docstring.

- Changes "Unkown role" to "Unknown role" in
`src/Lean/Elab/DocString.lean`
---
 src/Lean/Elab/DocString.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index 0ca292a482..c3fb817e38 100644
--- a/src/Lean/Elab/DocString.lean
+++ b/src/Lean/Elab/DocString.lean
@@ -1301,7 +1301,7 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
             continue
           else throw e
         | e => throw e
-    throwErrorAt name "Unkown role `{name}`"
+    throwErrorAt name "Unknown role `{name}`"
   | other =>
     throwErrorAt other "Unsupported syntax {other}"
 where