From 8e07e80f726478a80d20e270113c587b461a0a8e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 22 Jul 2022 13:28:37 +0200 Subject: [PATCH] feat: docComment parser alias --- src/Lean/Parser/Command.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 096efe0117..54c4bb73d7 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -153,6 +153,7 @@ builtin_initialize register_parser_alias declVal register_parser_alias optDeclSig register_parser_alias openDecl + register_parser_alias docComment end Command