# HG changeset patch
# User wenzelm
# Date 1650639348 -7200
# Node ID d1417d9c6debb0c5a3513d1912614fb82bc96bee
# Parent  691ed9f41729f972c92c7ee14a5bd8787fd4baeb
tuned signature: avoid problems with scala3;

diff -r 691ed9f41729 -r d1417d9c6deb src/Tools/jEdit/src/monitor_dockable.scala
--- 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) =>