From f20b212b72c511e89954506d834d993e1adecb23 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 15 Feb 2017 13:06:00 +0100
Subject: [PATCH] Remove warn_error(+8) from _tags

---
 _tags | 1 -
 1 file changed, 1 deletion(-)

diff --git a/_tags b/_tags
index 2edeeba1..31793d6e 100644
--- a/_tags
+++ b/_tags
@@ -29,7 +29,6 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 <src/smt/type_smt.*>: package(dolmen)
 
 # more warnings
-<src/**/*.ml>: warn_error(+8)
 <src/**/*.ml>: warn_K, warn_Y, warn_X
 <src/**/*.ml>: short_paths, safe_string, strict_sequence
 <src/**/*.cm*>: debug