aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 16:40:38 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 17:38:20 +0100
commit20e1829ad3de42dd322af972c6f9a585f40738ef (patch)
tree576a73f9a74fd4f80d8ae574ec1ba15847a4ad60 /lib
parenta6f1944809e4caa6c99deb8c508dab9ad0e0071e (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.ml2
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