# HG changeset patch
# User wenzelm
# Date 1261144808 -3600
# Node ID a4a457e393a4b5c9d73b8bcaf024ea443d96beb9
# Parent  3975494a4d8f0501243fd7ae1efc48398f7e1e6b
imitate PG 4 colors;

diff -r 3975494a4d8f -r a4a457e393a4 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
     }
   }