leanOutput Code action removes a `

[nomeata]

While writing a blog post I was regularly confused by strange syntax errors (missing end of file), and multiple times it turned out I had

```leanOutput foo
some outupt
``

in my file. Must have somehow deleted the `.

But right now I noticed that it was the code action that swallowed one of the `: When I have

```leanOutput evenInduct
```

and I run the code action it turns into

```leanOutput evenInduct
even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : ∀ (n : Nat), motive2 n → motive1 n.succ)
  (case3 : ∀ (n : Nat), motive1 n → motive2 n) : (∀ (n : Nat), motive1 n) ∧ ∀ (n : Nat), motive2 n
``

It does only seem to happen if the code block was empty to begin with.

Maybe an off-by-one-error somewhere, or removal of what was hoped to be a \n?

This is verso 93f84d7f89f1bbd7bcc0b79bb19d0b5f398f687e