--- a/src/Tools/jEdit/etc/options Mon Dec 10 10:41:29 2012 +0100
+++ b/src/Tools/jEdit/etc/options Mon Dec 10 13:52:33 2012 +0100
@@ -41,8 +41,8 @@
option quoted_color : string = "8B8B8B19"
option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
-option sendback_color : string = "DCDCDCFF"
-option sendback_active_color : string = "9DC75DFF"
+option active_color : string = "DCDCDCFF"
+option active_hover_color : string = "9DC75DFF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"