proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
authorwenzelm
Fri May 16 17:11:56 2014 +0200 (2014-05-16)
changeset 569809c5220e05e04
parent 56979 376604d56b54
child 56981 3ef45ce002b5
proper priority for error over warning, which got mixed up in 0546e036d1c0 and 4df2727a0b5f;
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri May 16 16:40:02 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri May 16 17:11:56 2014 +0200
     1.3 @@ -328,8 +328,8 @@
     1.4          val status = Protocol.Status.make(results.iterator.flatMap(_.info))
     1.5  
     1.6          if (status.is_running) Some(running_color)
     1.7 +        else if (status.is_failed) Some(error_color)
     1.8          else if (status.is_warned) Some(warning_color)
     1.9 -        else if (status.is_failed) Some(error_color)
    1.10          else if (status.is_unprocessed) Some(unprocessed_color)
    1.11          else None
    1.12        }