src/Pure/ML/ml_statistics.scala
changeset 51989 55f8bd61b029
parent 51870 3f9a24e7349e
     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"))