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 /kernel/type_errors.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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions