aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-05-19 20:18:03 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-05-19 20:22:16 +0200
commitd90b3c54ea8d26bf6fc48041cb1ca6cba5ba4c19 (patch)
treed10bb6573df2488f61ce0ce2d03e8a27335b4a5a /kernel/nativecode.ml
parent244d7a9aafe7ad613dd2095ca3126560cb3ea1d0 (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