src/Pure/ML/ml_statistics.scala
changeset 50974 55f8bd61b029
parent 50855 3f9a24e7349e
--- a/src/Pure/ML/ml_statistics.scala	Fri Jan 18 00:18:11 2013 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Fri Jan 18 16:20:09 2013 +0100
@@ -43,7 +43,8 @@
     ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
 
   val tasks_fields =
-    ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
+    ("Future tasks",
+      List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
 
   val workers_fields =
     ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))