max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing space after /--

Browse source
This commit is contained in:
Gabriel Ebner 2021-12-10 20:42:26 +01:00 • committed by Sebastian Ullrich
parent 4f81972996
commit b6efece612
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Parser/Term.lean
View file

@ -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