# HG changeset patch
# User wenzelm
# Date 1283105279 -7200
# Node ID 5c3e5c548f122a09a5dec08f45dc93a13f763e9c
# Parent  2f198d107aefa6fe3c6d565573851c992cbf5cd9
session_actor: ignore spurious TIMEOUT (again) -- probably stemming from earlier use of receiveWithin;

diff -r 2f198d107aef -r 5c3e5c548f12 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sun Aug 29 19:48:35 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Aug 29 20:07:59 2010 +0200
@@ -286,6 +286,8 @@
             finished = true
           }
 
+        case TIMEOUT =>  // FIXME clarify
+
         case bad if prover != null =>
           System.err.println("session_actor: ignoring bad message " + bad)
       }