author | wenzelm |
Tue, 30 Jun 2009 22:23:33 +0200 (2009-06-30) | |
changeset 31898 | 82d5190ff7c8 |
parent 31897 | 15d55d07de8b |
child 31899 | 1a7ade46061b |
child 31909 | d3b020134006 |
child 31963 | 663a725dc339 |
--- 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 ()))