# HG changeset patch
# User wenzelm
# Date 1263243661 -3600
# Node ID c1509b9d624f56e00a34e24be2a04f1f77e9807f
# Parent  f879b649ac4c1888711d7b0973336ffe80a4ebb4
tuned message;

diff -r f879b649ac4c -r c1509b9d624f src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Jan 11 21:37:48 2010 +0100
+++ b/src/Pure/library.scala	Mon Jan 11 22:01:01 2010 +0100
@@ -61,7 +61,7 @@
     val result = Exn.capture(e)
     val stop = System.currentTimeMillis()
     System.err.println(
-      (if (message.isEmpty) "" else message + " ") + (stop - start) + "ms elapsed time")
+      (if (message.isEmpty) "" else message + ": ") + (stop - start) + "ms elapsed time")
     Exn.release(result)
   }
 }