diff --git a/_tags b/_tags index acfe0b21..a5e1a655 100644 --- a/_tags +++ b/_tags @@ -13,6 +13,6 @@ # more warnings <**/*.ml>: warn_K, warn_Y, warn_X -<**/*.ml>: keep_locks, short_paths, safe_string, strict_sequence +<**/*.ml>: short_paths, safe_string, strict_sequence <**/*.cm*>: debug