author | wenzelm |
Sun, 29 Aug 2010 20:07:59 +0200 | |
changeset 38850 | 5c3e5c548f12 |
parent 38849 | 2f198d107aef |
child 38851 | 227dd9a9459a |
--- 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) }