| changeset 55790 | 4670f18baba5 |
| parent 55747 | bef19c929ba5 |
| child 55919 | 2eb8c13339a5 |
--- a/src/Tools/jEdit/etc/options Thu Feb 27 17:39:20 2014 +0100 +++ b/src/Tools/jEdit/etc/options Thu Feb 27 17:56:59 2014 +0100 @@ -59,7 +59,6 @@ option unprocessed1_color : string = "FFA0A032" option running_color : string = "610061FF" option running1_color : string = "61006164" -option light_color : string = "F0F0F064" option bullet_color : string = "000000FF" option tooltip_color : string = "FFFFE9FF" option writeln_color : string = "C0C0C0FF"