--- a/src/Tools/jEdit/etc/options Fri Sep 14 17:37:19 2012 +0200
+++ b/src/Tools/jEdit/etc/options Fri Sep 14 18:12:41 2012 +0200
@@ -32,9 +32,9 @@
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
option bad_color : string = "FF6A6A64"
-option hilite_color : string = "FFCC6664"
+option intensify_color : string = "FFCC6664"
option quoted_color : string = "8B8B8B19"
-option subexp_color : string = "50505032"
+option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"