diff options
| author | Gaëtan Gilbert | 2019-03-12 19:06:17 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-18 13:02:31 +0100 |
| commit | 0c34281b682cb4416c131d22f70426999500d977 (patch) | |
| tree | 07dfbc17e009f24ae347bdcc04858ec2fbb6e116 /plugins/syntax/string_notation.ml | |
| parent | 9ac5483132b42e845a0708491843693b70893eef (diff) | |
Don't lose the warning name when warning becomes error.
Diffstat (limited to 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions