diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-12 17:15:06 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-13 18:59:32 +0200 |
| commit | 2938fceb50b71d4784d6d718021c505c00196f50 (patch) | |
| tree | 44068df44063367b6a2554f1234a435aeec5e84b /vernac/mltop.ml | |
| parent | 240c8bffaa788669cf3135c95d067cc7b11b5da1 (diff) | |
Complying more precisely to unicode standard.
In particular, checking that it is at most 4 bytes.
Diffstat (limited to 'vernac/mltop.ml')
0 files changed, 0 insertions, 0 deletions