From 7ba82ed9f595c7d93bd40846993c2447572a817a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 2 Nov 2016 15:54:37 +0100 Subject: Put string between quotes when printing an option value. This is a better (more generic) fix to #5061 than my e8b9ee76. --- library/goptions.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/goptions.ml b/library/goptions.ml index 35616558a..dfb3c0e69 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -381,9 +381,9 @@ let msg_option_value (name,v) = | BoolValue false -> str "off" | IntValue (Some n) -> int n | IntValue None -> str "undefined" - | StringValue s -> str s + | StringValue s -> str "\"" ++ str s ++ str "\"" | StringOptValue None -> str"undefined" - | StringOptValue (Some s) -> str s + | StringOptValue (Some s) -> str "\"" ++ str s ++ str "\"" (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = -- cgit v1.2.3