From fa24d2da6f33076ddd73d88812841f5f0cbffc6c Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 5 Oct 2015 15:18:42 +0200
Subject: [PATCH] Small _tags update

---
 _tags | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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