tuned message;
authorwenzelm
Tue, 08 Jun 2021 23:36:30 +0200
changeset 73839 0638fa8c01bc
parent 73838 0e6a5a6cc767
child 73840 a5200fa7cb4c
tuned message;
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", "")
     }
   }