# HG changeset patch
# User wenzelm
# Date 1246393413 -7200
# Node ID 82d5190ff7c820c7c57cc2fb54967c426a0c899e
# Parent  15d55d07de8b3f606c0307c0debc771e45ee000f
more detailed timing message;

diff -r 15d55d07de8b -r 82d5190ff7c8 src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Tue Jun 30 22:12:46 2009 +0200
+++ b/src/Pure/System/session.ML	Tue Jun 30 22:23:33 2009 +0200
@@ -103,7 +103,10 @@
           val start = start_timing ();
           val _ = use root;
           val stop = end_timing start;
-          val _ = Output.std_error ("Timing " ^ item ^ " (" ^ #message stop ^ ")\n");
+          val _ =
+            Output.std_error ("Timing " ^ item ^ " (" ^
+              string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
+              #message stop ^ ")\n");
         in () end
       else use root;
       finish ()))