diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean index 08afb2d..7011238 100644 --- 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