diff --git a/_tags b/_tags index fd66075..831c1ef 100644 --- a/_tags +++ b/_tags @@ -29,6 +29,7 @@ # OASIS_STOP true: bin_annot, color(always) <**/*.ml>: warn(+a-4-44-48@8) +: warn(-33) true: mark_tag_used <**/*.cmx>: optimize(3) : nolabels