leanOutput Code action removes a `

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

Reproduce the issue using the leanOutput code action on an empty leanOutput block, using the example with evenInduct. Trace the code action's handling of the opening and closing backticks and compare its output with the original block. Done means the generated output preserves valid Markdown fences and no longer removes a backtick.