src/Pure/General/mailman.scala

--- a/src/Pure/General/mailman.scala	Fri Feb 24 20:40:50 2023 +0100
+++ b/src/Pure/General/mailman.scala	Fri Feb 24 20:52:35 2023 +0100
@@ -453,9 +453,7 @@
 
     def get(lines: List[String]): List[String] =
       unapply(lines) getOrElse
-        error("Missing delimiters:" +
-          (if (bg.nonEmpty) " " else "") + bg +
-          (if (en.nonEmpty) " " else "") + en)
+        error("Missing delimiters:" + if_proper(bg, " ") + bg + if_proper(en, " ") + en)
   }