# HG changeset patch
# User wenzelm
# Date 1407000542 -7200
# Node ID d8966c09025c20674baa4b07cb78bcc54ab0d664
# Parent  8e4ae2db184936c08cf12aa88051ce6c82c958cd
proper priority for error over warning also for node_status (see 9c5220e05e04);

diff -r 8e4ae2db1849 -r d8966c09025c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Sat Aug 02 16:35:59 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Sat Aug 02 19:29:02 2014 +0200
@@ -145,8 +145,8 @@
       val status = Status.merge(states.iterator.map(_.protocol_status))
 
       if (status.is_running) running += 1
+      else if (status.is_failed) failed += 1
       else if (status.is_warned) warned += 1
-      else if (status.is_failed) failed += 1
       else if (status.is_finished) finished += 1
       else unprocessed += 1
     }