# HG changeset patch
# User wenzelm
# Date 1222986108 -7200
# Node ID 500ff7219782661b51956fd8e1870a7487d9c297
# Parent  00046e3b46b5360f89ac453e0a382c5df90c6d1b
tuned tracing;

diff -r 00046e3b46b5 -r 500ff7219782 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Fri Oct 03 00:12:13 2008 +0200
+++ b/src/Pure/Concurrent/future.ML	Fri Oct 03 00:21:48 2008 +0200
@@ -151,7 +151,8 @@
     val _ = trace_active ();
     val _ = Multithreading.tracing 3 (fn () => name ^ ": running");
     val ok = setmp_thread_data (name, task, group) run ();
-    val _ = Multithreading.tracing 3 (fn () => name ^ ": finished");
+    val _ = Multithreading.tracing 3
+      (fn () => name ^ ": finished " ^ (if ok then "(ok)" else "(failed)"));
     val _ = SYNCHRONIZED "execute" (fn () =>
      (change queue (TaskQueue.finish task);
       if ok then ()