diff options
| author | Emilio Jesus Gallego Arias | 2020-06-02 13:43:26 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-02 13:43:26 +0200 |
| commit | d495815dfc5b4113c2ebcd83b4319dc4dabc3f66 (patch) | |
| tree | 84a7912dadb51cd19d31ddc3ee7e8372e4dd7a63 /ide/utf8_convert.mll | |
| parent | a1fa186fc8314e395a0813bb23c2c73d738b7572 (diff) | |
| parent | 083ab9fb9ac3b63d741e342cfb2a847968a6784e (diff) | |
Merge PR #11974: Require in Section: warning is now about fragility not deprecation.
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'ide/utf8_convert.mll')
0 files changed, 0 insertions, 0 deletions