proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
--- 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
}