--- a/src/Pure/Admin/build_status.scala Thu May 18 14:38:09 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Thu May 18 14:41:20 2017 +0200
@@ -356,7 +356,9 @@
(if (session.ml_statistics.content.nonEmpty)
List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) :::
(if (session.threads > 1)
- List(jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields))
+ List(
+ jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields),
+ jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields))
else Nil)
else Nil)