--- 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))