From b6efece612818d4a2b6bf92f73a59d0bb60f1931 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 10 Dec 2021 20:42:26 +0100 Subject: [PATCH] fix: missing space after /-- --- src/Lean/Parser/Term.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 2ca3496630..e9e884aa44 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -16,7 +16,7 @@ def commentBody : Parser := @[combinatorParenthesizer Lean.Parser.Command.commentBody] def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken @[combinatorFormatter Lean.Parser.Command.commentBody] def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous -def docComment := leading_parser ppDedent $ "/--" >> commentBody >> ppLine +def docComment := leading_parser ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine end Command builtin_initialize