From ed09ae7a473a99c914f2af64d3387d9190e85849 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 15 Dec 2017 04:15:55 +0100 Subject: [flags] Move global time flag into an attribute. One less global flag. --- lib/system.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'lib/system.mli') diff --git a/lib/system.mli b/lib/system.mli index c02bc9c8a..0c0cc9fae 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -104,4 +104,4 @@ val get_time : unit -> time val time_difference : time -> time -> float (** in seconds *) val fmt_time_difference : time -> time -> Pp.t -val with_time : bool -> ('a -> 'b) -> 'a -> 'b +val with_time : batch:bool -> ('a -> 'b) -> 'a -> 'b -- cgit v1.2.3