src/Pure/General/mailman.scala
changeset 77368 7c57d9586f4c
parent 75906 2167b9e3157a
child 77369 df17355f1e2c
--- 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))) }