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