author | wenzelm |
Wed, 10 Jul 2013 20:16:04 +0200 | |
changeset 52576 | 7f5be9be51a7 |
parent 52575 | e78ea835b5f8 |
child 52577 | a9ae6534dc5c |
--- a/src/Tools/jEdit/etc/options Wed Jul 10 13:43:23 2013 +0200 +++ b/src/Tools/jEdit/etc/options Wed Jul 10 20:16:04 2013 +0200 @@ -38,7 +38,7 @@ option unprocessed1_color : string = "FFA0A032" option running_color : string = "610061FF" option running1_color : string = "61006164" -option light_color : string = "F0F0F0FF" +option light_color : string = "F0F0F064" option bullet_color : string = "000000FF" option tooltip_color : string = "FFFFE9FF" option writeln_color : string = "C0C0C0FF"