1.1 --- a/src/Pure/ML/ml_statistics.scala Fri Jan 18 00:18:11 2013 +0100
1.2 +++ b/src/Pure/ML/ml_statistics.scala Fri Jan 18 16:20:09 2013 +0100
1.3 @@ -43,7 +43,8 @@
1.4 ("Time", List("time_GC_system", "time_GC_user", "time_non_GC_system", "time_non_GC_user"))
1.5
1.6 val tasks_fields =
1.7 - ("Future tasks", List("tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
1.8 + ("Future tasks",
1.9 + List("tasks_proof", "tasks_ready", "tasks_pending", "tasks_running", "tasks_passive"))
1.10
1.11 val workers_fields =
1.12 ("Worker threads", List("workers_total", "workers_active", "workers_waiting"))