joinSep and line breaks

Stream: lean4

[Damiano Testa]

Is the printing behaviour below what I should expect?

import Lean.Elab.Command

open Lean

/--
info: a
b
---
info: a
b
a b
-/
#guard_msgs in
run_cmd
  let msg := m!"a\nb"
  logInfo <| .joinSep [msg] "\n"
  logInfo <| .joinSep [msg, msg] "\n"

[Mario Carneiro]

The formatter doesn't like it when you put newlines in the atomic strings it manipulates, I'm not sure whether it preprocesses them to replace the newlines with line breaks

[Damiano Testa]

Ok, thanks!

I still find it funny that it only does that for the trailing string/MessageData, except when the list is a singleton. Anyway, I can certainly live with this or split line breaks into longer lists, I was just surprised by the outcome.