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