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/spawn.ml | |
| 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/spawn.ml')
0 files changed, 0 insertions, 0 deletions