src/Pure/PIDE/command.scala
changeset 59203 5f0bd5afc16d
parent 59072 27c6936c6484
child 59684 86a76300137e
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Dec 30 14:11:06 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Dec 30 23:45:03 2014 +0100
     1.3 @@ -128,7 +128,7 @@
     1.4      lazy val protocol_status: Protocol.Status =
     1.5      {
     1.6        val warnings =
     1.7 -        if (results.iterator.exists(p => Protocol.is_warning(p._2)))
     1.8 +        if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2)))
     1.9            List(Markup(Markup.WARNING, Nil))
    1.10          else Nil
    1.11        val errors =