changeset 61590 | 94ab348eaab2 |
parent 60074 | 38a64cc17403 |
child 61724 | 4bfcc09a33e8 |
--- a/src/Tools/jEdit/src/monitor_dockable.scala Fri Nov 06 14:43:05 2015 +0100 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Fri Nov 06 18:15:35 2015 +0100 @@ -22,7 +22,7 @@ class Monitor_Dockable(view: View, position: String) extends Dockable(view, position) { - private val rev_stats = Synchronized(Nil: List[Properties.T]) + private val rev_stats = Synchronized[List[Properties.T]](Nil) /* chart data -- owned by GUI thread */