From abad0a15ac44cb5b53b87382bb4d587d9800a0f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 3 Jul 2014 12:43:28 +0200
Subject: time tac

---
 lib/system.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/system.mli')

diff --git a/lib/system.mli b/lib/system.mli
index 2e286a40c..9cfb1456f 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -67,3 +67,5 @@ type time
 val get_time : unit -> time
 val time_difference : time -> time -> float (** in seconds *)
 val fmt_time_difference : time -> time -> Pp.std_ppcmds
+
+val with_time : bool -> ('a -> 'b) -> 'a -> 'b
-- 
cgit v1.2.3