diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index e1c2d5c1af..5dc1c956ed 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -456,7 +456,7 @@ partial def finishCommentBlock (nesting : Nat) : ParserFn := fun c s => if nesting == 1 then s.next' input i h else finishCommentBlock (nesting-1) c (s.next' input i h) else - finishCommentBlock nesting c (s.next input i) + finishCommentBlock nesting c (s.setPos i) else if curr == '/' then if h : input.atEnd i then eoi s else diff --git a/tests/lean/run/1883.lean b/tests/lean/run/1883.lean new file mode 100644 index 0000000000..0290e8be70 --- /dev/null +++ b/tests/lean/run/1883.lean @@ -0,0 +1,3 @@ +/-- this docstring doesn't end with minus-slash as it should --/ + +def foo : Nat := 37