diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 17:46:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 17:46:53 +0200 |
| commit | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (patch) | |
| tree | 92ce430c64b7bea374b926d81acc5433d39fdcbb /library/goptions.ml | |
| parent | f79f2b32da8e5e443428d4f642216ddfb404857c (diff) | |
| parent | a18fb93587ccbe32a2edfad38d2e9095f6c8e901 (diff) | |
Merge branch 'v8.6'
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/goptions.ml b/library/goptions.ml index 0459417fb..1cf25987b 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -365,8 +365,8 @@ let set_string_option_value = set_string_option_value_gen None let msg_option_value (name,v) = match v with - | BoolValue true -> str "true" - | BoolValue false -> str "false" + | BoolValue true -> str "on" + | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" | StringValue s -> str s |