diff options
| author | Maxime Dénès | 2017-06-20 11:09:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-23 10:32:19 +0200 |
| commit | 965960bcd13eb3a6e531b03fb85be516dcdca551 (patch) | |
| tree | c790d157d6a51dd714b3fe33c7c08c86e29c834a /kernel/nativelambda.ml | |
| parent | 409f73f6e69b7c62ae3bdf1686fa3cc9ccc06e9f (diff) | |
Fix bug 5392: Warnings defined in plugins are considered unknown
The status of a warning can now be set before the warning is declared
(typically by a plugin). However, I had to remove the "unknown warning"
warning.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions