changeset 41776 | 3bd83302a3c3 |
parent 41737 | 1b225934c09d |
child 42128 | eb84d28961a9 |
--- a/src/Pure/Concurrent/future.ML Fri Feb 18 16:07:32 2011 +0100 +++ b/src/Pure/Concurrent/future.ML Fri Feb 18 16:11:58 2011 +0100 @@ -203,7 +203,7 @@ Task_Queue.running task (fn () => setmp_worker_task task (fn () => fold (fn job => fn ok => job valid andalso ok) jobs true) ()); - val _ = Multithreading.tracing 1 (fn () => + val _ = Multithreading.tracing 2 (fn () => let val s = Task_Queue.str_of_task task; fun micros time = string_of_int (Time.toNanoseconds time div 1000);