diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-13 18:05:12 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 20:22:17 +0200 |
commit | 561349466556f02b8d2e1cb8f2b846c188243bf9 (patch) | |
tree | adad932b0aafc320f8acde9f5664c589cbb109d7 /lib/cString.mli | |
parent | 81ee9f1cb152a82cc4c116dd47294f2ae6eee0ed (diff) |
Extra warning about unicode character of unknown status following an ident.
This covers the case e.g. of "xₚ" (until the table of unicode
characters is upgraded!).
Diffstat (limited to 'lib/cString.mli')
0 files changed, 0 insertions, 0 deletions