mllib: use Unix.gettimeofday instead of Unix.time

Unix.gettimeofday returns a finer resolution than seconds, which is what
we need since deciseconds of timestamps are printed.
This commit is contained in:
Pino Toscano
2015-06-03 16:13:43 +02:00
parent 14a8461a5c
commit fa80f88c9c

View File

@@ -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;