From e3f4e068c13395773f006fa7dda44c42293024ba Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 14 Sep 2017 09:18:33 +0200 Subject: [PATCH] remove spurious warning --- _tags | 1 + 1 file changed, 1 insertion(+) 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