diff -r d27d1224c67f -r 7c57d9586f4c src/Pure/General/mailman.scala --- a/src/Pure/General/mailman.scala Fri Feb 24 20:23:48 2023 +0100 +++ b/src/Pure/General/mailman.scala Fri Feb 24 20:40:50 2023 +0100 @@ -541,7 +541,7 @@ override def message_content(name: String, lines: List[String]): Message = { def err(msg: String = ""): Nothing = - error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg)) + error("Malformed message: " + name + if_proper(msg, "\n" + msg)) val (head, body) = try { (Head.get(lines), make_body(Body.get(lines))) } @@ -596,7 +596,7 @@ override def message_content(name: String, lines: List[String]): Message = { def err(msg: String = ""): Nothing = - error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg)) + error("Malformed message: " + name + if_proper(msg, "\n" + msg)) val (head, body) = try { (Head.get(lines), make_body(Body.get(lines))) }