# HG changeset patch
# User wenzelm
# Date 1385052337 -3600
# Node ID 41e4ba92a9792c06d0ed87e4585133fb16e1dc4b
# Parent  483131676087620895373bcdd5b465c8747effb2
proper concatenation of messages;

diff -r 483131676087 -r 41e4ba92a979 src/Pure/library.scala
--- a/src/Pure/library.scala	Wed Nov 20 23:14:06 2013 +0100
+++ b/src/Pure/library.scala	Thu Nov 21 17:45:37 2013 +0100
@@ -26,9 +26,12 @@
 
   def error(message: String): Nothing = throw ERROR(message)
 
+  def cat_message(msg1: String, msg2: String): String =
+    if (msg1 == "") msg2
+    else msg1 + "\n" + msg2
+
   def cat_error(msg1: String, msg2: String): Nothing =
-    if (msg1 == "") error(msg1)
-    else error(msg1 + "\n" + msg2)
+    error(cat_message(msg1, msg2))
 
 
   /* separated chunks */