From 6ffbe4308229feb63525506e6a1fa77a61d2895b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 4 Oct 2016 13:05:58 +0200 Subject: Changing the separator for appended string options to comma. This is a bit ad-hoc, but looks better for warnings since there is a command-line flag accepting the same values, so comma will lead to fewer parsing issues than space. --- library/goptions.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'library/goptions.ml') diff --git a/library/goptions.ml b/library/goptions.ml index 2876d6243..35616558a 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -305,7 +305,7 @@ let declare_string_option = declare_option (fun v -> StringValue v) (function StringValue v -> v | _ -> anomaly (Pp.str "async_option")) - (fun x y -> x^" "^y) + (fun x y -> x^","^y) let declare_stringopt_option = declare_option (fun v -> StringOptValue v) -- cgit v1.2.3