# HG changeset patch
# User wenzelm
# Date 1308166215 -7200
# Node ID 40c67d894be461d53615c4628e9b72d39d0da93f
# Parent  723a8af9d3f06643cfc9deda9ceb71b511bb7894
avoid compiler warning -- this is unchecked anyway;

diff -r 723a8af9d3f0 -r 40c67d894be4 src/Pure/System/event_bus.scala
--- a/src/Pure/System/event_bus.scala	Wed Jun 15 21:22:51 2011 +0200
+++ b/src/Pure/System/event_bus.scala	Wed Jun 15 21:30:15 2011 +0200
@@ -20,7 +20,7 @@
   def + (r: Actor): Event_Bus[Event] = { this += r; this }
 
   def += (f: Event => Unit) {
-    this += actor { loop { react { case x: Event => f(x) } } }
+    this += actor { loop { react { case x => f(x.asInstanceOf[Event]) } } }
   }
 
   def + (f: Event => Unit): Event_Bus[Event] = { this += f; this }