aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-09-28 16:19:23 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-09-28 16:34:21 +0200
commita75770eb41e8a3bbfb44cb65d04bb3af29448fe7 (patch)
tree2de3f36abd006b58d7e4a8f89efca0a4116abaf4 /kernel/nativelib.ml
parentdaae678047ee2a1c53d4dc423976f77e40ba753f (diff)
CLEANUP: remove the definition of the "CString.map" function. We will use the official "String.map" function instead.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions