diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-24 18:43:12 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-24 22:04:26 +0100 |
| commit | aa560c640eb3f1148c87c4343900138845729105 (patch) | |
| tree | 709db53a99baabbe8f7984396d86128b70dd4f8a /vernac | |
| parent | c1e670b386f83ed78104a6eb6e4d17cc1d906439 (diff) | |
[lib] Generalize Control.timeout type.
We also remove some internal implementation details from the mli file,
there due historical reasons.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 62c7edb19..9a67aa6dd 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2144,7 +2144,7 @@ let vernac_timeout f = match !current_timeout, !default_timeout with | Some n, _ | None, Some n -> let f () = f (); current_timeout := None in - Control.timeout n f Timeout + Control.timeout n f () Timeout | None, None -> f () let restore_timeout () = current_timeout := None |