equal
deleted
inserted
replaced
17 |
17 |
18 option jedit_tooltip_dismiss_delay : real = 8.0 |
18 option jedit_tooltip_dismiss_delay : real = 8.0 |
19 -- "global delay for Swing tooltips" |
19 -- "global delay for Swing tooltips" |
20 |
20 |
21 |
21 |
22 section {* Editor document view *} |
22 section "Editor Document View" |
23 |
23 |
24 option color_outdated : string = "EEE3E3FF" |
24 option color_outdated : string = "EEE3E3FF" |
25 option color_unprocessed : string = "FFA0A0FF" |
25 option color_unprocessed : string = "FFA0A0FF" |
26 option color_unprocessed1 : string = "FFA0A032" |
26 option color_unprocessed1 : string = "FFA0A032" |
27 option color_running : string = "610061FF" |
27 option color_running : string = "610061FF" |