src/Tools/Graphview/mutator_event.scala
changeset 61590 94ab348eaab2
parent 59442 9f45b95d3543
child 73340 0ffcad1f6130
--- a/src/Tools/Graphview/mutator_event.scala	Fri Nov 06 14:43:05 2015 +0100
+++ b/src/Tools/Graphview/mutator_event.scala	Fri Nov 06 18:15:35 2015 +0100
@@ -21,7 +21,7 @@
 
   class Bus
   {
-    private val receivers = Synchronized(List.empty[Receiver])
+    private val receivers = Synchronized[List[Receiver]](Nil)
 
     def += (r: Receiver) { receivers.change(Library.insert(r)) }
     def -= (r: Receiver) { receivers.change(Library.remove(r)) }