| changeset 49706 | 92ef8b638c6c |
| parent 49701 | e2762f962042 |
| child 49722 | c91419b3a425 |
--- a/src/Tools/jEdit/etc/options Fri Oct 05 10:54:07 2012 +0200 +++ b/src/Tools/jEdit/etc/options Fri Oct 05 11:09:24 2012 +0200 @@ -30,6 +30,7 @@ option running_color : string = "610061FF" option running1_color : string = "61006164" option light_color : string = "F0F0F0FF" +option tooltip_color : string = "FFFFE9FF" option writeln_color : string = "C0C0C0FF" option warning_color : string = "FF8C00FF" option error_color : string = "B22222FF"