| changeset 47390 | 580c37559354 |
| parent 47346 | cd3ab7625519 |
| child 47629 | 645163d3b964 |
--- a/src/Pure/System/session.scala Sat Apr 07 16:41:59 2012 +0200 +++ b/src/Pure/System/session.scala Sat Apr 07 16:59:27 2012 +0200 @@ -399,7 +399,7 @@ case _ => if (output.is_exit && phase == Session.Startup) phase = Session.Failed else if (output.is_exit) phase = Session.Inactive - else if (output.is_stdout) { } + else if (output.is_init || output.is_stdout) { } else bad_output(output) } }