diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-08-30 09:34:10 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-08-30 09:37:08 +0200 |
commit | 64e801cce80ac0d3bffcebf414d57785a2c6826f (patch) | |
tree | 645e329d85de7b34dbf3080b0048408a1719e116 /library/goptions.ml | |
parent | 513e194656429b6a9142a3a34095cee2c6f8ee96 (diff) |
Setting an unknown option now always a warning. Fixes #4947.
Previously, setting an unknown option was an error or a warning,
depending on the type of the option. We make it always a warning, for
forward compatibility.
This was already fixed in 8.6.
Diffstat (limited to 'library/goptions.ml')
-rw-r--r-- | library/goptions.ml | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 5f6512e11..97da8a1ea 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -304,18 +304,18 @@ let declare_stringopt_option = (* Setting values of options *) let set_option_value locality check_and_cast key v = - let (name, depr, (_,read,write,lwrite,gwrite)) = - try get_option key - with Not_found -> - errorlabstrm "Goptions.set_option_value" - (str "There is no option " ++ str (nickname key) ++ str ".") - in - let write = match locality with - | None -> write - | Some true -> lwrite - | Some false -> gwrite - in - write (check_and_cast v (read ())) + let opt = try Some (get_option key) with Not_found -> None in + match opt with + | None -> + msg_warning + (str "There is no option " ++ str (nickname key) ++ str ".") + | Some (name, depr, (_,read,write,lwrite,gwrite)) -> + let write = match locality with + | None -> write + | Some true -> lwrite + | Some false -> gwrite + in + write (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -345,13 +345,11 @@ let check_unset_value v = function let set_int_option_value_gen locality = set_option_value locality check_int_value let set_bool_option_value_gen locality key v = - try set_option_value locality check_bool_value key v - with UserError (_,s) -> msg_warning s + set_option_value locality check_bool_value key v let set_string_option_value_gen locality = set_option_value locality check_string_value let unset_option_value_gen locality key = - try set_option_value locality check_unset_value key () - with UserError (_,s) -> msg_warning s + set_option_value locality check_unset_value key () let set_int_option_value = set_int_option_value_gen None let set_bool_option_value = set_bool_option_value_gen None |