diff options
| author | Maxime Dénès | 2016-11-02 15:54:37 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-02 16:05:07 +0100 |
| commit | 7ba82ed9f595c7d93bd40846993c2447572a817a (patch) | |
| tree | 7b41fa32282ce07aca47db4d74b2718a6cf0097b /plugins/syntax/string_syntax.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 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions