aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorEnrico Tassi2016-09-30 11:08:47 +0200
committerEnrico Tassi2016-09-30 11:08:47 +0200
commit69d43e7615f080c2e4e57a87e84b51be857ab678 (patch)
tree6ec8c9e43a3e035cab88018c113e7b840965d882 /kernel/nativelambda.ml
parent775b8f28562d1d5063da2b28a06e59610b76f06f (diff)
Restore code ignoring <W> lines in output (camlp5 warnings)
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions