aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-22 07:30:50 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-22 07:31:03 +0200
commit246a5011d7a794835aa0f9ca198b3a4a74031ed6 (patch)
tree94a1818dafc31a18b21adfbdb242b2f3d8eb4c7a /kernel/cemitcodes.ml
parent3d5b210d4148e1edb9f7a02c888decf9cc6c30e6 (diff)
Remove obsolete documentation. (Fix bug #4238)
Diffstat (limited to 'kernel/cemitcodes.ml')
0 files changed, 0 insertions, 0 deletions