From 64e801cce80ac0d3bffcebf414d57785a2c6826f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 30 Aug 2016 09:34:10 +0200 Subject: 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. --- library/goptions.ml | 30 ++++++++++++++---------------- 1 file 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 -- cgit v1.2.3