# HG changeset patch
# User wenzelm
# Date 1623188190 -7200
# Node ID 0638fa8c01bc7b942d070c894dfb11df5d5f3a97
# Parent  0e6a5a6cc767246010bfa10a062c19817d25854f
tuned message;

diff -r 0e6a5a6cc767 -r 0638fa8c01bc src/Pure/ML/ml_profiling.scala
--- a/src/Pure/ML/ml_profiling.scala	Tue Jun 08 23:34:06 2021 +0200
+++ b/src/Pure/ML/ml_profiling.scala	Tue Jun 08 23:36:30 2021 +0200
@@ -32,7 +32,7 @@
     def print: String =
     {
       (if (kind == "time_thread") "time profile (single thread)" else kind + " profile") +
-        (entries ::: List(total)).map(_.print).mkString(":\n", "\n", "\n")
+        (entries ::: List(total)).map(_.print).mkString(":\n", "\n", "")
     }
   }