diff options
| author | Pierre-Marie Pédrot | 2021-01-14 19:12:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-14 19:12:11 +0100 |
| commit | eb25e63d58555a67b74a046b8bdf2ab6252164c0 (patch) | |
| tree | b3deef1089255b400e66cb540c315d629aff4108 /lib/control.mli | |
| parent | b8a3ebaa9695596f062298f5913ae4f4debb0124 (diff) | |
| parent | 00a09f2cc4a8f4b6baeca0a474e5ab4062ff0f97 (diff) | |
Merge PR #13378: Add support for high resolution timeout functions
Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot
Diffstat (limited to 'lib/control.mli')
| -rw-r--r-- | lib/control.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/control.mli b/lib/control.mli index 9465d8f0d5..f992d8e8d0 100644 --- a/lib/control.mli +++ b/lib/control.mli @@ -24,13 +24,13 @@ val check_for_interrupt : unit -> unit (** Use this function as a potential yield function. If {!interrupt} has been set, il will raise [Sys.Break]. *) -val timeout : int -> ('a -> 'b) -> 'a -> 'b option +val timeout : float -> ('a -> 'b) -> 'a -> 'b option (** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so before [n] seconds, returns [None] instead. *) (** Set a particular timeout function; warning, this is an internal API and it is scheduled to go away. *) -type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option } +type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> 'b option } val set_timeout : timeout -> unit (** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that |