diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 17:16:53 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-09 17:16:53 +0100 |
| commit | 3b4bae6246b780961aa49b81a074e77189252bb3 (patch) | |
| tree | 1fe0006899d6e09f54b960e42c576f13747f5d77 /ide | |
| parent | 5542ffe43dde333cec6d118fd4b0424313330c33 (diff) | |
| parent | a8297dd69f840a23740e7b36f852522d7c3471f9 (diff) | |
Merge PR #6923: Export options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 0ba1b3a4f..55b4fa87e 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -57,8 +57,8 @@ let coqide_known_option table = List.mem table [ ["Printing";"Unfocused"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (o,BoolValue true) - | VernacUnsetOption o -> coqide_known_option o + | VernacSetOption (_, o, BoolValue true) + | VernacUnsetOption (_, o) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) @@ -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 |