# HG changeset patch
# User wenzelm
# Date 1333810767 -7200
# Node ID 580c37559354b59168f3ce9826bd318c84879fc0
# Parent  e8552cba702d6c7978e9b7de078e27d9d2e1ac9e
init message not bad;

diff -r e8552cba702d -r 580c37559354 src/Pure/System/session.scala
--- 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)
       }
     }