From 3443e2b8dc16d9dffce72015b385b2ae3379e592 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 4 Nov 2014 20:42:43 +0100 Subject: [PATCH] optimization in Log.debug --- util/log.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/util/log.ml b/util/log.ml index 07e41416..cd5cfc95 100644 --- a/util/log.ml +++ b/util/log.ml @@ -27,15 +27,16 @@ OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. let debug_level_ = ref 0 let set_debug l = debug_level_ := l let get_debug () = !debug_level_ +let _dummy_buf = Buffer.create 0 (* dummy buffer, never used *) let debug l format = - let b = Buffer.create 15 in if l <= !debug_level_ then ( + let b = Buffer.create 64 in Printf.kbprintf (fun b -> print_endline (Buffer.contents b)) b format) else - Printf.ifprintf b format + Printf.ifprintf _dummy_buf format let on_buffer pp x = let buf = Buffer.create 24 in