diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-04 13:05:58 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-04 13:05:58 +0200 |
| commit | 6ffbe4308229feb63525506e6a1fa77a61d2895b (patch) | |
| tree | 9458866c3f2bbd50f51881e1e76be48d870c542b /library/goptions.ml | |
| parent | 5838f198019651455b62e1ab588f6f72d0c036f4 (diff) | |
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.
Diffstat (limited to 'library/goptions.ml')
| -rw-r--r-- | library/goptions.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |