diff -r 34ac36642a31 -r 0fa351b1bd14 src/Tools/jEdit/etc/options
--- 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"