From e872f76058e954fac3e0652ec567aff72226e9dd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Dec 2016 11:03:12 +0100
Subject: [pp] Debug feeder is not needed anymore.

-> Candidate to be merge with the main feedback commit.
---
 lib/feedback.ml  | 4 ----
 lib/feedback.mli | 3 ---
 2 files changed, 7 deletions(-)

(limited to 'lib')

diff --git a/lib/feedback.ml b/lib/feedback.ml
index 31677ecfc9..7d9d6bf7f0 100644
--- a/lib/feedback.ml
+++ b/lib/feedback.ml
@@ -79,7 +79,3 @@ let msg_notice  ?loc x = feedback_logger ?loc Notice x
 let msg_warning ?loc x = feedback_logger ?loc Warning x
 let msg_error   ?loc x = feedback_logger ?loc Error x
 let msg_debug   ?loc x = feedback_logger ?loc Debug x
-
-let debug_feeder = function
-  | { contents = Message (Debug, loc, pp) } -> msg_debug ?loc pp
-  | _ -> ()
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 3fb7c0039e..4bbdfcb5b6 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -64,9 +64,6 @@ val add_feeder : (feedback -> unit) -> int
 (** [del_feeder fid] removes the feeder with id [fid] *)
 val del_feeder : int -> unit
 
-(** Prints feedback messages of kind Message(Debug,_) using msg_debug *)
-val debug_feeder : feedback -> unit
-
 (** [feedback ?id ?route fb] produces feedback fb, with [route] and
     [id] set appropiatedly, if absent, it will use the defaults set by
     [set_id_for_feedback] *)
-- 
cgit v1.2.3