Unix.gettimeofday returns a finer resolution than seconds, which is what we need since deciseconds of timestamps are printed. --- mllib/common_utils.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/mllib/common_utils.ml b/mllib/common_utils.ml index 32e908d..516cff3 100644 --- a/mllib/common_utils.ml +++ b/mllib/common_utils.ml @@ -282,11 +282,11 @@ let verbose () = !verbose (* Timestamped progress messages, used for ordinary messages when not * --quiet. *) -let start_t = Unix.time () +let start_t = Unix.gettimeofday () let message fs = let display str = if not (quiet ()) then ( - let t = sprintf "%.1f" (Unix.time () -. start_t) in + let t = sprintf "%.1f" (Unix.gettimeofday () -. start_t) in printf "[%6s] " t; ansi_green (); printf "%s" str; -- 2.1.0