author | wenzelm |
Fri, 22 Apr 2022 16:55:48 +0200 | |
changeset 75447 | d1417d9c6deb |
parent 75446 | 691ed9f41729 |
child 75448 | 53a60eae475f |
--- a/src/Tools/jEdit/src/monitor_dockable.scala Fri Apr 22 16:47:13 2022 +0200 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Fri Apr 22 16:55:48 2022 +0200 @@ -28,7 +28,7 @@ private var statistics_length = 0 private def add_statistics(stats: Properties.T): Unit = { - statistics = statistics.enqueue(stats) + statistics = statistics.appended(stats) statistics_length += 1 limit_data.text match { case Value.Int(limit) =>