diff options
| author | Lasse Blaauwbroek | 2020-11-22 11:22:52 +0100 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-12-06 16:56:07 +0100 |
| commit | 00a09f2cc4a8f4b6baeca0a474e5ab4062ff0f97 (patch) | |
| tree | 63884d6459014a889739ee9583ceb7d8d9d648e9 /vernac/vernacinterp.ml | |
| parent | 7514bc25c6e8dffeb58ae9af0916dac83953d337 (diff) | |
Add support for high resolution timeout functions.
Diffstat (limited to 'vernac/vernacinterp.ml')
| -rw-r--r-- | vernac/vernacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index e5971e1aaa..3a8a80d25a 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -82,7 +82,7 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b = match !default_timeout, timeout with | _, Some n | Some n, None -> - (match Control.timeout n f x with + (match Control.timeout (float_of_int n) f x with | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout) | Some x -> x) | None, None -> |