From 4e2595df8983f64cb094334f8b4e2851e3f837fa Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 16 Jun 2016 21:23:36 +0200 Subject: [PATCH] add optimize() flag to _tags --- _tags | 1 + 1 file changed, 1 insertion(+) diff --git a/_tags b/_tags index 6158cde..493c238 100644 --- a/_tags +++ b/_tags @@ -30,4 +30,5 @@ true: bin_annot <**/*.ml>: warn_A, warn(-4) true: mark_tag_used +<**/*.cmx>: optimize(3) : nolabels