diff options
| author | Maxime Dénès | 2017-12-22 15:55:01 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-12-22 15:55:01 +0100 |
| commit | 3e8ad7726320de5b954675026a4ae429c6c324a8 (patch) | |
| tree | 448ab6903267de8cd8bbc68cb3a35693561ec191 /ide | |
| parent | 2a056809bcd025ab59791e4f839c91c8361b77c4 (diff) | |
| parent | 28d45c2413ad24c758fca5cfb00ec4ba20935f39 (diff) | |
Merge PR #6318: Separate vernac controls and regular commands.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 58599a14dc..aafc3fc59a 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -54,7 +54,7 @@ let coqide_known_option table = List.mem table [ ["Printing";"Universes"]; ["Printing";"Unfocused"]] -let is_known_option cmd = match cmd with +let is_known_option cmd = match Vernacprop.under_control cmd with | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> coqide_known_option o | _ -> false |