changeset 57843 | d8966c09025c |
parent 56801 | 8dd9df88f647 |
child 57911 | dcb758188aa6 |
--- 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 }