src/Tools/jEdit/src/rendering.scala
changeset 55713 734ac5709fbe
parent 55710 2d623ab55672
child 55746 97f390fa0f3a
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 12:23:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Feb 24 12:51:55 2014 +0100
     1.3 @@ -260,6 +260,7 @@
     1.4    val keyword1_color = color_value("keyword1_color")
     1.5    val keyword2_color = color_value("keyword2_color")
     1.6    val keyword3_color = color_value("keyword3_color")
     1.7 +  val caret_invisible_color = color_value("caret_invisible_color")
     1.8  
     1.9    val tfree_color = color_value("tfree_color")
    1.10    val tvar_color = color_value("tvar_color")