more charts;
authorwenzelm
Thu May 18 14:41:20 2017 +0200 (2017-05-18)
changeset 6586753613acb76e7
parent 65866 00e8b836d4db
child 65868 65e132abab1e
more charts;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu May 18 14:38:09 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu May 18 14:41:20 2017 +0200
     1.3 @@ -356,7 +356,9 @@
     1.4                  (if (session.ml_statistics.content.nonEmpty)
     1.5                    List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) :::
     1.6                    (if (session.threads > 1)
     1.7 -                    List(jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields))
     1.8 +                    List(
     1.9 +                      jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields),
    1.10 +                      jfreechart(plot_name("workers_chart"), ML_Statistics.workers_fields))
    1.11                     else Nil)
    1.12                   else Nil)
    1.13