From ea1757875a14c434bffb12b49b189bea65df0412 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 5 Nov 2014 15:56:37 +0100 Subject: [PATCH] Now building with debug flag --- _tags | 2 ++ 1 file changed, 2 insertions(+) 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