src/Tools/jEdit/etc/options
changeset 65101 4263b2a201b3
parent 64835 fd1efd6dd385
child 65141 c706b57b1694
equal deleted inserted replaced
65100:83d1f210a1d3 65101:4263b2a201b3
   142 option inner_cartouche_color : string = "CC6600FF"
   142 option inner_cartouche_color : string = "CC6600FF"
   143 option inner_comment_color : string = "CC0000FF"
   143 option inner_comment_color : string = "CC0000FF"
   144 option dynamic_color : string = "7BA428FF"
   144 option dynamic_color : string = "7BA428FF"
   145 option class_parameter_color : string = "D2691EFF"
   145 option class_parameter_color : string = "D2691EFF"
   146 
   146 
   147 option markdown_item_color1 : string = "DAFEDAFF"
   147 option markdown_item1_color : string = "DAFEDAFF"
   148 option markdown_item_color2 : string = "FFF0CCFF"
   148 option markdown_item2_color : string = "FFF0CCFF"
   149 option markdown_item_color3 : string = "E7E7FFFF"
   149 option markdown_item3_color : string = "E7E7FFFF"
   150 option markdown_item_color4 : string = "FFE0F0FF"
   150 option markdown_item4_color : string = "FFE0F0FF"
   151 
   151 
   152 
   152 
   153 section "Icons"
   153 section "Icons"
   154 
   154 
   155 option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
   155 option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"