diff options
| author | Emilio Jesus Gallego Arias | 2017-04-18 22:59:28 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-18 22:59:28 +0200 |
| commit | fb4d7b0cf48e2be82b9975492b23fbd46e2087ad (patch) | |
| tree | b39c82573e314190d164041576206871d8600c5c /kernel/type_errors.mli | |
| parent | beb3acd2fd3831404f0be2da61d3f28e210e8349 (diff) | |
[toplevel] Fix #5475
This was a logic error in 63cfc77ddf3586262d905dc351b58669d185a55e,
`Notice`-level messages should not be wrapped in `<infomsg>` tags.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions