Lean LSP inserts comment delimiters after return

Stream: lean4

[Leni Aniva]

I don't know if this is because of my settings (which I have left as the default) or it occurs for everyone. I use Lean4 plugin for Emacs. If I have some code like this

/-
comment
-/
def mystery (a: Nat) := a + 1

when I try to insert a new line after comment, I get

/-
comment-/
/-
-/
def mystery (a: Nat) := a + 1

Two additional comment delimiters get inserted automatically. How can I prevent this from happening? It gets very annoying when I type multi-line comments

[Jannis Limperg]

I set comment-multi-line t in lean4-mode, which seems to make Emacs's behaviour slightly less annoying. I tried to fully fix the issue at some point, but didn't manage.

[Paul Nelson]

How are you attempting to insert a newline? I only get the behavior you describe using default-indent-new-line (bound to M-j for me), and not via newline (bound to RET for me).

[Leni Aniva]

Paul Nelson said:

How are you attempting to insert a newline? I only get the behavior you describe using default-indent-new-line (bound to M-j for me), and not via newline (bound to RET for me).

same, but my keybinding binds RET to default-indent-new-line