chore: remove dbg_trace

leanprover · Dec 18, 2024 · 3008d9e · 3008d9e
1 parent 573d97f
commit 3008d9e
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
@@ -844,7 +844,6 @@ def tryElabInlineCodeName (str : String) : DocElabM Term := do
   if x.toString == str then
     let stx := mkIdent x
     let n ← realizeGlobalConstNoOverload stx
-    dbg_trace "NAME {n} worked for {str}"
     let hl : Highlighted ← constTok n str
     ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hl)) #[Verso.Doc.Inline.code $(quote str)])
   else