diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-11-02 15:54:37 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-11-02 16:05:07 +0100 |
| commit | 7ba82ed9f595c7d93bd40846993c2447572a817a (patch) | |
| tree | 7b41fa32282ce07aca47db4d74b2718a6cf0097b /library/goptions.ml | |
| parent | 0d06d69ffc0436ed326bf3e4c684dc17a4d85dde (diff) | |
Put string between quotes when printing an option value.
This is a better (more generic) fix to #5061 than my e8b9ee76.
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 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 = |