--- 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))) }