From 9bff82239c2a6412a26ae3c5faab42a9c9d2ccb1 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 24 Jun 2016 18:51:32 +0200
Subject: [feedback] Remove unused tag on `Debug` level.

IMO level indicators are not the proper place to store this information.
---
 lib/feedback.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib/feedback.mli')

diff --git a/lib/feedback.mli b/lib/feedback.mli
index 50ffd22db..690877897 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -10,7 +10,7 @@ open Xml_datatype
 
 (* Old plain messages (used to be in Pp) *)
 type level =
-  | Debug of string
+  | Debug
   | Info
   | Notice
   | Warning
-- 
cgit v1.2.3