diff --git a/_tags b/_tags index 37a53b13..2026ea27 100644 --- a/_tags +++ b/_tags @@ -160,4 +160,5 @@ : thread : thread : -traverse +: inline(25) <{string,core}/**/*.ml>: warn_A, warn(-4), warn(-44)