--- 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"))