Newlines are stripped by `m!`

Stream: lean4

[Eric Wieser]

Is this deliberate behavior for docs#Lean.MessageData interpolation?

import Lean

#eval Lean.logInfo <| f!"Newline\nplease"  --ok
#eval Lean.logInfo <| Std.Format.group <| f!"Newline\nplease"  --ok

#eval Lean.logInfo <| m!"Newline\nplease"  --ok
#eval Lean.logInfo <| Lean.MessageData.group <| m!"Newline\nplease"  --no newline

[Eric Wieser]

(If you look at the generated term, m! is sneakily replacing \n with Format.line)