aboutsummaryrefslogtreecommitdiff
path: root/lib/control.ml
diff options
context:
space:
mode:
authorMaxime Dénès2018-12-12 09:57:09 +0100
committerMaxime Dénès2018-12-12 09:57:09 +0100
commitd87c4c472478fbcb30de6efabc68473ee36849a1 (patch)
tree5b4e1cb66298db57b978374422822ffdf2673100 /lib/control.ml
parent850dfbf59f52b0d3dcba237ee2af5ce99fd1bcd2 (diff)
parentd00472c59d15259b486868c5ccdb50b6e602a548 (diff)
Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.
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 3fbeb168c4..e09068740d 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -62,8 +62,8 @@ let windows_timeout n f x e =
let res = f x in
let () = killed := true in
let cur = Unix.gettimeofday () in
- (** The thread did not interrupt, but the computation took longer than
- expected. *)
+ (* The thread did not interrupt, but the computation took longer than
+ expected. *)
let () = if float_of_int n <= cur -. init then begin
exited := true;
raise Sys.Break
@@ -71,7 +71,7 @@ let windows_timeout n f x e =
res
with
| Sys.Break ->
- (** Just in case, it could be a regular Ctrl+C *)
+ (* Just in case, it could be a regular Ctrl+C *)
if not !exited then begin killed := true; raise Sys.Break end
else raise e
| e ->