imitate PG 4 colors;
authorwenzelm
Fri, 18 Dec 2009 15:00:08 +0100
changeset 34794 a4a457e393a4
parent 34793 3975494a4d8f
child 34795 c97335b7e8c3
imitate PG 4 colors;
src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Dec 18 12:29:30 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Dec 18 15:00:08 2009 +0100
@@ -28,7 +28,7 @@
     command.status(doc) match {
       case Command.Status.UNPROCESSED => new Color(255, 228, 225)
       case Command.Status.FINISHED => new Color(234, 248, 255)
-      case Command.Status.FAILED => new Color(255, 106, 106)
+      case Command.Status.FAILED => new Color(255, 193, 193)
       case _ => Color.red
     }
   }