diff options
Diffstat (limited to 'toplevel/vernac.ml')
| -rw-r--r-- | toplevel/vernac.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 934cddb4f..84e20f5ed 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -61,6 +61,7 @@ let default_timeout = ref None let _ = Goptions.declare_int_option { Goptions.optsync = true; + Goptions.optdepr = false; Goptions.optname = "the default timeout"; Goptions.optkey = ["Default";"Timeout"]; Goptions.optread = (fun () -> !default_timeout); |