From 38a671f74857aec8e285a6a0bfcab876e3b9a133 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Feb 2018 13:26:53 +0100 Subject: Export the various option localities in the API. This prevents relying on an underspecified bool option argument. --- ide/ide_slave.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'ide') diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0ba1b3a4f..9fe580091 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -340,7 +340,7 @@ let set_options options = | IntValue i -> Goptions.set_int_option_value name i | StringValue s -> Goptions.set_string_option_value name s | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen None name + | StringOptValue None -> Goptions.unset_option_value_gen name in List.iter iter options -- cgit v1.2.3