diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 94f9c9a36..041f2f83b 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -291,11 +291,13 @@ let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b | Goptions.IntValue x -> Interface.IntValue x | Goptions.StringValue s -> Interface.StringValue s + | Goptions.StringOptValue s -> Interface.StringOptValue s let import_option_value = function | Interface.BoolValue b -> Goptions.BoolValue b | Interface.IntValue x -> Goptions.IntValue x | Interface.StringValue s -> Goptions.StringValue s + | Interface.StringOptValue s -> Goptions.StringOptValue s let export_option_state s = { Interface.opt_sync = s.Goptions.opt_sync; @@ -314,6 +316,8 @@ let set_options options = | BoolValue b -> Goptions.set_bool_option_value name b | 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 in List.iter iter options |