# HG changeset patch
# User wenzelm
# Date 1674916716 -3600
# Node ID 34a6b8bd7abd804df7a0a24a8ba3f2ba4f973ae4
# Parent  f07d6bcbefa82cac0663648315496a44caf0f961
tuned;

diff -r f07d6bcbefa8 -r 34a6b8bd7abd src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Sat Jan 28 15:35:43 2023 +0100
+++ b/src/Pure/ML/ml_statistics.scala	Sat Jan 28 15:38:36 2023 +0100
@@ -285,7 +285,7 @@
     data.removeAllSeries()
     for (field <- selected_fields) {
       val series = new XYSeries(field)
-      content.foreach(entry => series.add(entry.time, entry.get(field)))
+      content.foreach(e => series.add(e.time, e.get(field)))
       data.addSeries(series)
     }
   }