From 8a095f2298e9add1e39609ef83d84677f1f717c2 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Wed, 17 Sep 2014 23:09:17 +0200 Subject: [PATCH] ignore sequence/ dir --- _tags | 1 + 1 file changed, 1 insertion(+) diff --git a/_tags b/_tags index 9bdfa3d1..e89e7e22 100644 --- a/_tags +++ b/_tags @@ -159,4 +159,5 @@ # OASIS_STOP : thread : thread +: -traverse <{string,core}/**/*.ml>: warn_K, warn_Y, warn_X