remove spurious warning

This commit is contained in:
Simon Cruanes 2017-09-14 09:18:33 +02:00
parent d59d96a513
commit e3f4e068c1

1
_tags
View file

@ -29,6 +29,7 @@
# OASIS_STOP # OASIS_STOP
true: bin_annot, color(always) true: bin_annot, color(always)
<**/*.ml>: warn(+a-4-44-48@8) <**/*.ml>: warn(+a-4-44-48@8)
<src/bigarray/*.ml>: warn(-33)
true: mark_tag_used true: mark_tag_used
<**/*.cmx>: optimize(3) <**/*.cmx>: optimize(3)
<src/sequenceLabels.cm*>: nolabels <src/sequenceLabels.cm*>: nolabels