comment parsing ignores #exit

[robertylewis]

#exit 
/- 

complains about "unexpected end of comment block" on line 2. Obviously not a big deal, but a little surprising!

Even more surprising: start with this.

#exit 
/- 

Then change it to this:

#exit 
/- 
-/
#eval 2

The evaluation happens! Restarting the Lean server makes it behave as expected, with no messages after #exit.

Reproduced on 3.15.0.

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

[Description of the issue]

Steps to Reproduce

1. [First Step]
2. [Second Step]
3. [and so on...]

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

You can get this information from copy and pasting the output of lean --version,
please include the OS and what version of the OS you're running.

Additional Information

Any additional information, configuration or data that might be necessary to reproduce the issue.