diff --git a/_tags b/_tags index a9971c2..b391676 100644 --- a/_tags +++ b/_tags @@ -29,3 +29,4 @@ # OASIS_STOP true: bin_annot <**/*.ml>: warn_A, warn(-4) +true: mark_tag_used