proper priority for error over warning also for node_status (see 9c5220e05e04);
authorwenzelm
Sat, 02 Aug 2014 19:29:02 +0200
changeset 59059d8966c09025c
parent 59058 8e4ae2db1849
child 59060 ae3eac418c5f
proper priority for error over warning also for node_status (see 9c5220e05e04);
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sat Aug 02 16:35:59 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Sat Aug 02 19:29:02 2014 +0200
     1.3 @@ -145,8 +145,8 @@
     1.4        val status = Status.merge(states.iterator.map(_.protocol_status))
     1.5  
     1.6        if (status.is_running) running += 1
     1.7 +      else if (status.is_failed) failed += 1
     1.8        else if (status.is_warned) warned += 1
     1.9 -      else if (status.is_failed) failed += 1
    1.10        else if (status.is_finished) finished += 1
    1.11        else unprocessed += 1
    1.12      }