aboutsummaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-10-17 17:24:32 +0200
committerPierre-Marie Pédrot2016-10-17 17:24:58 +0200
commit409bc943e8d8a0bc0d35ae63f3530b7324ca975e (patch)
tree2c40c07aeb5bfdd4a331b2961c37b862d16e9576 /kernel/cemitcodes.mli
parent13a2d032004f9678aec84eb5e1ef11c98e43aa9f (diff)
Fix previous commit.
I've messed up with parts of the compatibility files I had to commit.
Diffstat (limited to 'kernel/cemitcodes.mli')
0 files changed, 0 insertions, 0 deletions