aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-09-06 18:42:52 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-09-06 18:55:25 +0200
commit977e91d0aa5cfece962fc82e3fd42402918663c8 (patch)
tree756a4bc293d50bc9b1831ae017707e312bdf50e7 /library
parent83ec679e785f5313f088be77bcd652a29783623b (diff)
A proposal to unify the messages given by Test and Print Options (#5062).
Diffstat (limited to 'library')
-rw-r--r--library/goptions.ml4
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