tuned signature: avoid problems with scala3;
authorwenzelm
Fri, 22 Apr 2022 16:55:48 +0200
changeset 75447 d1417d9c6deb
parent 75446 691ed9f41729
child 75448 53a60eae475f
tuned signature: avoid problems with scala3;
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) =>