--- a/src/Pure/System/session.scala Mon Jul 29 14:18:57 2013 +0200
+++ b/src/Pure/System/session.scala Mon Jul 29 14:37:59 2013 +0200
@@ -461,7 +461,7 @@
if (rc == 0) phase = Session.Inactive
else phase = Session.Failed
- case _ => bad_output()
+ case _ => raw_output_messages.event(output)
}
}
}