1551 |
strings_of_option display_downloaded_results; |
strings_of_option display_downloaded_results; |
1552 |
strings_of_option vd_reload_delay; |
strings_of_option vd_reload_delay; |
1553 |
strings_of_option html_use_gzip; |
strings_of_option html_use_gzip; |
1554 |
|
strings_of_option html_mods_use_js_tooltips; |
1555 |
|
strings_of_option html_mods_js_tooltips_wait; |
1556 |
|
strings_of_option html_mods_js_tooltips_timeout; |
1557 |
] @ (if Autoconf.has_gd then |
] @ (if Autoconf.has_gd then |
1558 |
[strings_of_option html_mods_vd_gfx;] else []) @ |
[strings_of_option html_mods_vd_gfx;] else []) @ |
1559 |
(if Autoconf.has_gd_jpg && Autoconf.has_gd_png |
(if Autoconf.has_gd_jpg && Autoconf.has_gd_png |