diff options
Diffstat (limited to 'toplevel/whelp.ml4')
| -rw-r--r-- | toplevel/whelp.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4 index 3fd114afe..aa38e9e9f 100644 --- a/toplevel/whelp.ml4 +++ b/toplevel/whelp.ml4 @@ -38,6 +38,7 @@ open Goptions let _ = declare_string_option { optsync = false; + optdepr = false; optname = "Whelp server"; optkey = ["Whelp";"Server"]; optread = (fun () -> !whelp_server_name); @@ -46,6 +47,7 @@ let _ = let _ = declare_string_option { optsync = false; + optdepr = false; optname = "Whelp getter"; optkey = ["Whelp";"Getter"]; optread = (fun () -> !getter_server_name); |