From 74fc940f3e64b5a91c1a932114af6db598e39ae8 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 10 Jan 2015 21:11:11 +0100 Subject: [PATCH] detail in _tags --- _tags | 1 + 1 file changed, 1 insertion(+) 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