parsing error for `set_option` after docstring comment

Stream: lean4

[Arien Malec]

#mwe

-- /-- multiline
-- comment-/ -- if you uncomment this, syntax error
set_option linter.deprecated false in
theorem bar {α β: Type _}: α = β := sorry

-- this position is OK
--set_option linter.deprecated false in
/-- multiline
comment-/
set_option linter.deprecated false in -- syntax error
def foo {α :Type _} : α -> α := sorry

[Mario Carneiro]

yes this is expected behavior

[Reid Barton]

That's a docstring, not (just) a multiline comment, since it starts with /--

[Reid Barton]

/- this is a
multiline comment -/