diff options
Diffstat (limited to 'lib/profile.ml')
| -rw-r--r-- | lib/profile.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/lib/profile.ml b/lib/profile.ml index d154478177..cde5ed5999 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -15,8 +15,7 @@ let float_of_time t = float_of_int t /. 100. let time_of_float f = int_of_float (f *. 100.) let get_time () = - let {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in - time_of_float (ut +. st) + time_of_float (Sys.time ()) (* Since ocaml 3.01, gc statistics are in float *) let get_alloc () = @@ -155,7 +154,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) = (* Unix measure of time is approximative and shoitt delays are often unperceivable; therefore, total times are measured in one (big) step to avoid rounding errors and to get the best possible - approximation *) + approximation. + Note: Sys.time is the same as: + Unix.(let x = times () in x.tms_utime +. x.tms_stime) + *) (* ---------- start profile for f1 |