aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-11-05 17:15:37 -0500
committerMatthieu Sozeau2015-11-11 19:13:52 +0100
commit67da4b45ef65db59b2d7ba1549351d792e1b27d9 (patch)
tree96afc8bd7b6ce2136bb2e9bf15b8f4db7bc67ea8 /kernel/nativecode.mli
parentca30a8be08beeae77d42b6cb5d9f219e3932a3f7 (diff)
Fix bug #3735: interpretation of "->" in Program follows the standard one.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions