diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 16:40:38 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 17:38:20 +0100 |
commit | 20e1829ad3de42dd322af972c6f9a585f40738ef (patch) | |
tree | 576a73f9a74fd4f80d8ae574ec1ba15847a4ad60 /lib | |
parent | a6f1944809e4caa6c99deb8c508dab9ad0e0071e (diff) |
Fixing compilation with OCaml 3.12 after commit 9d45d45f3a87 on removing
"open Unix" from lib/system.ml.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/system.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml index f860bd2f7..a90222960 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -262,7 +262,7 @@ type time = float * float * float let get_time () = let t = Unix.times () in - (Unix.gettimeofday(), t.tms_utime, t.tms_stime) + (Unix.gettimeofday(), t.Unix.tms_utime, t.Unix.tms_stime) (* Keep only 3 significant digits *) let round f = (floor (f *. 1e3)) *. 1e-3 |