diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-19 20:18:03 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-05-19 20:22:16 +0200 |
| commit | d90b3c54ea8d26bf6fc48041cb1ca6cba5ba4c19 (patch) | |
| tree | d10bb6573df2488f61ce0ce2d03e8a27335b4a5a /kernel/nativecode.ml | |
| parent | 244d7a9aafe7ad613dd2095ca3126560cb3ea1d0 (diff) | |
Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions