src/Tools/jEdit/etc/options
changeset 49418 c451856129cd
parent 49358 0fa351b1bd14
child 49473 ca7e2c21b104
equal deleted inserted replaced
49417:c5a8592fb5d3 49418:c451856129cd
    29 option light_color : string = "F0F0F0FF"
    29 option light_color : string = "F0F0F0FF"
    30 option writeln_color : string = "C0C0C0FF"
    30 option writeln_color : string = "C0C0C0FF"
    31 option warning_color : string = "FF8C00FF"
    31 option warning_color : string = "FF8C00FF"
    32 option error_color : string = "B22222FF"
    32 option error_color : string = "B22222FF"
    33 option error1_color : string = "B2222232"
    33 option error1_color : string = "B2222232"
       
    34 option writeln_message_color : string = "F0F0F0FF"
       
    35 option tracing_message_color : string = "F0F8FFFF"
       
    36 option warning_message_color : string = "EEE8AAFF"
       
    37 option error_message_color : string = "FFC1C1FF"
    34 option bad_color : string = "FF6A6A64"
    38 option bad_color : string = "FF6A6A64"
    35 option intensify_color : string = "FFCC6664"
    39 option intensify_color : string = "FFCC6664"
    36 option quoted_color : string = "8B8B8B19"
    40 option quoted_color : string = "8B8B8B19"
    37 option highlight_color : string = "50505032"
    41 option highlight_color : string = "50505032"
    38 option hyperlink_color : string = "000000FF"
    42 option hyperlink_color : string = "000000FF"