src/Pure/System/session.scala
changeset 38230 ed147003de4b
parent 38227 6bbb42843b6e
child 38260 d4a1c7a19be3
     1.1 --- a/src/Pure/System/session.scala	Sat Aug 07 21:22:39 2010 +0200
     1.2 +++ b/src/Pure/System/session.scala	Sat Aug 07 22:09:52 2010 +0200
     1.3 @@ -138,7 +138,7 @@
     1.4      {
     1.5        raw_results.event(result)
     1.6  
     1.7 -      val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
     1.8 +      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
     1.9        val target: Option[Session.Entity] =
    1.10          target_id match {
    1.11            case None => None