aboutsummaryrefslogtreecommitdiff
path: root/lib/control.ml
diff options
context:
space:
mode:
authorMaxime Dénès2017-07-21 17:14:29 +0200
committerMaxime Dénès2017-07-21 17:14:29 +0200
commitc0fdb912c5e63bb43d6e8dd320e9f5613c6237ff (patch)
treeab0e7f43c58a2554f78f317893eb69120dae5dd4 /lib/control.ml
parentf30269579b78d5bf65dcd5db70e341fe9598b274 (diff)
parent5b3d0f2cd7a5f480fe24a938e2f6713798c7139a (diff)
Merge PR #897: Fix test suite on windows (wrt fake_ide and coq-makefile)
Diffstat (limited to 'lib/control.ml')
-rw-r--r--lib/control.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/control.ml b/lib/control.ml
index d9b91be3a0..f5d7df204e 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -48,7 +48,7 @@ let windows_timeout n f e =
let exited = ref false in
let thread init =
while not !killed do
- let cur = Unix.time () in
+ let cur = Unix.gettimeofday () in
if float_of_int n <= cur -. init then begin
interrupt := true;
exited := true;
@@ -57,12 +57,12 @@ let windows_timeout n f e =
Thread.delay 0.5
done
in
- let init = Unix.time () in
+ let init = Unix.gettimeofday () in
let _id = Thread.create thread init in
try
let res = f () in
let () = killed := true in
- let cur = Unix.time () in
+ let cur = Unix.gettimeofday () in
(** The thread did not interrupt, but the computation took longer than
expected. *)
let () = if float_of_int n <= cur -. init then begin