diff --git a/_tags b/_tags index 8508f50a..813c5403 100644 --- a/_tags +++ b/_tags @@ -8,3 +8,5 @@ # more warnings <**/*.ml>: warn_K, warn_Y, warn_X + +<**/*.cm*>: debug