infoview "copy message to comment" looses stuff

[joneugster]

See Zulip.

In the following example, the infoview button "copy message to comment" copies an incomplete error message to context.

import Mathlib

example : 1 + 1 = 2 := Nat.add_one

[joneugster]

Seems to be specific to error messages.

In the following, it works fine:

import Mathlib

example : 1 + 1 = 2 := Nat.add_one _

[abentkamp]

We'll need a new release of the @leanprover/infoview npm package. I have written to Wojciech about this.