diff options
| author | Emilio Jesus Gallego Arias | 2019-03-20 01:56:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-20 01:56:42 +0100 |
| commit | cc8e8e8e37603e69e85e68fb00df0ac28faac971 (patch) | |
| tree | 66c0da47795ff97e0da3770fae554b36307e6e11 /plugins/syntax/string_notation.mli | |
| parent | 19bb153e049dcd7bd3ce4780e9fe18ec1d3a1169 (diff) | |
| parent | 0c34281b682cb4416c131d22f70426999500d977 (diff) | |
Merge PR #9754: Don't lose the warning name when warning becomes error.
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions