changeset 56980 | 9c5220e05e04 |
parent 56883 | 38c6b70e5e53 |
child 57594 | 037f3b251df5 |
--- a/src/Tools/jEdit/src/rendering.scala Fri May 16 16:40:02 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Fri May 16 17:11:56 2014 +0200 @@ -328,8 +328,8 @@ val status = Protocol.Status.make(results.iterator.flatMap(_.info)) if (status.is_running) Some(running_color) + else if (status.is_failed) Some(error_color) else if (status.is_warned) Some(warning_color) - else if (status.is_failed) Some(error_color) else if (status.is_unprocessed) Some(unprocessed_color) else None }