changeset 38850 | 5c3e5c548f12 |
parent 38849 | 2f198d107aef |
child 38882 | e1fb3bbc22ab |
--- 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) }