Merge branch 'v8.6'

1 files changed, 6 insertions, 5 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 8f2f06925..7ddf46bdd 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -247,7 +247,7 @@ let get_locality = function
   | Some false -> OptGlobal
   | None -> OptDefault
 
-let declare_option cast uncast append
+let declare_option cast uncast append ?(preprocess = fun x -> x)
   { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
@@ -275,10 +275,11 @@ let declare_option cast uncast append
             subst_function = subst_options;
             discharge_function = discharge_options;
             classify_function = classify_options } in
-      (fun l m v -> Lib.add_anonymous_leaf (options (l, m, v)))
+      (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v)))
     else
       (fun _ m v ->
-       match m with
+        let v = preprocess v in
+        match m with
        | OptSet -> write v
        | OptAppend -> write (append (read ()) v))
   in
@@ -381,9 +382,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 =