--- a/src/Pure/General/markup.scala Tue Sep 07 15:03:59 2010 +0200 +++ b/src/Pure/General/markup.scala Tue Sep 07 16:08:29 2010 +0200 @@ -249,6 +249,8 @@ val SIGNAL = "signal" val EXIT = "exit" + val BAD = "bad" + val Ready = Markup("ready", Nil)