From 73201a4e6714f1ebf55e79238f15abe667061379 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 6 Nov 2014 13:48:03 +0100 Subject: [PATCH] add some warnings (to be fixed) --- _tags | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/_tags b/_tags index e89e7e22..5a3bb15a 100644 --- a/_tags +++ b/_tags @@ -160,4 +160,4 @@ : thread : thread : -traverse -<{string,core}/**/*.ml>: warn_K, warn_Y, warn_X +<{string,core}/**/*.ml>: warn_A, warn(-4)