src/Tools/jEdit/etc/options
changeset 52576 7f5be9be51a7
parent 52472 3a43a8b1ecb0
child 52643 34c29356930e
equal deleted inserted replaced
52575:e78ea835b5f8 52576:7f5be9be51a7
    36 option outdated_color : string = "EEE3E3FF"
    36 option outdated_color : string = "EEE3E3FF"
    37 option unprocessed_color : string = "FFA0A0FF"
    37 option unprocessed_color : string = "FFA0A0FF"
    38 option unprocessed1_color : string = "FFA0A032"
    38 option unprocessed1_color : string = "FFA0A032"
    39 option running_color : string = "610061FF"
    39 option running_color : string = "610061FF"
    40 option running1_color : string = "61006164"
    40 option running1_color : string = "61006164"
    41 option light_color : string = "F0F0F0FF"
    41 option light_color : string = "F0F0F064"
    42 option bullet_color : string = "000000FF"
    42 option bullet_color : string = "000000FF"
    43 option tooltip_color : string = "FFFFE9FF"
    43 option tooltip_color : string = "FFFFE9FF"
    44 option writeln_color : string = "C0C0C0FF"
    44 option writeln_color : string = "C0C0C0FF"
    45 option warning_color : string = "FF8C00FF"
    45 option warning_color : string = "FF8C00FF"
    46 option error_color : string = "B22222FF"
    46 option error_color : string = "B22222FF"