diff options
Diffstat (limited to 'otherlibs/unix/unix.ml')
| -rw-r--r-- | otherlibs/unix/unix.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/otherlibs/unix/unix.ml b/otherlibs/unix/unix.ml index b3c2d0072..b2d7d124b 100644 --- a/otherlibs/unix/unix.ml +++ b/otherlibs/unix/unix.ml @@ -277,6 +277,7 @@ external time : unit -> int = "unix_time" external gettimeofday : unit -> float = "unix_gettimeofday" external gmtime : int -> tm = "unix_gmtime" external localtime : int -> tm = "unix_localtime" +external mktime : tm -> int * tm = "unix_mktime" external alarm : int -> int = "unix_alarm" external sleep : int -> unit = "unix_sleep" external times : unit -> process_times = |