diff options
| author | Maxime Dénès | 2016-10-04 13:05:58 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-04 13:05:58 +0200 |
| commit | 6ffbe4308229feb63525506e6a1fa77a61d2895b (patch) | |
| tree | 9458866c3f2bbd50f51881e1e76be48d870c542b /interp/notation_ops.mli | |
| 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 'interp/notation_ops.mli')
0 files changed, 0 insertions, 0 deletions