634 |
let html_use_gzip = define_expert_option current_section |
let html_use_gzip = define_expert_option current_section |
635 |
["html_use_gzip"] "Use gzip compression on web pages" bool_option false |
["html_use_gzip"] "Use gzip compression on web pages" bool_option false |
636 |
|
|
637 |
|
let html_mods_use_js_tooltips = define_expert_option current_section |
638 |
|
["html_mods_use_js_tooltips"] "Whether to use the fancy javascript tooltips or plain html-title" bool_option true |
639 |
|
|
640 |
|
let html_mods_js_tooltips_wait = define_expert_option current_section |
641 |
|
["html_mods_js_tooltips_wait"] "How long to wait before displaying the tooltips" int_option 0 |
642 |
|
|
643 |
|
let html_mods_js_tooltips_timeout = define_expert_option current_section |
644 |
|
["html_mods_js_tooltips_timeout"] "How long to display the tooltips" int_option 100000 |
645 |
|
|
646 |
|
|
647 |
(*************************************************************************) |
(*************************************************************************) |