diff options
| author | Maxime Dénès | 2016-11-03 17:55:37 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-03 17:55:37 +0100 |
| commit | 0c01a177362f8d7408ba8906fe0cba1948d8fb9c (patch) | |
| tree | ee84a305e691da2d6c87eb830c4b94376f2f19e1 /plugins/syntax | |
| parent | df1720bff67889818f8b4856f29ac02540d7f756 (diff) | |
| parent | 2c5eef988f11979175de6d1983bc533ce18b1095 (diff) | |
Merge remote-tracking branch 'github/pr/340' into v8.6
Was PR#340: Fix various shortcomings of the warnings infrastructure.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions