# HG changeset patch
# User wenzelm
# Date 1357218657 -3600
# Node ID 373093ffcbda8de2ddb5f9f8d33fba0caa4ca65a
# Parent  49621c7550750d9b969c6fccd56738e3c0a1d930
more interesting fields;

diff -r 49621c755075 -r 373093ffcbda src/Tools/jEdit/src/monitor_dockable.scala
--- a/src/Tools/jEdit/src/monitor_dockable.scala	Thu Jan 03 14:03:44 2013 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala	Thu Jan 03 14:10:57 2013 +0100
@@ -29,7 +29,7 @@
   private val delay_update =
     Swing_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) {
       ML_Statistics(rev_stats.reverse)
-        .update_data(data, ML_Statistics.tasks_fields._2)  // FIXME selectable fields
+        .update_data(data, ML_Statistics.workers_fields._2) // FIXME selectable fields
     }
 
   set_content(new ChartPanel(chart))