diff options
Diffstat (limited to 'otherlibs/unix/unix.ml')
| -rw-r--r-- | otherlibs/unix/unix.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/otherlibs/unix/unix.ml b/otherlibs/unix/unix.ml index 1d0761516e..4097be0b8a 100644 --- a/otherlibs/unix/unix.ml +++ b/otherlibs/unix/unix.ml @@ -437,8 +437,10 @@ type tm = tm_yday : int; tm_isdst : bool } -external time : unit -> float = "unix_time" -external gettimeofday : unit -> float = "unix_gettimeofday" +external time : unit -> (float [@unboxed]) = + "unix_time" "unix_time_unboxed" [@@noalloc] +external gettimeofday : unit -> (float [@unboxed]) = + "unix_gettimeofday" "unix_gettimeofday_unboxed" [@@noalloc] external gmtime : float -> tm = "unix_gmtime" external localtime : float -> tm = "unix_localtime" external mktime : tm -> float * tm = "unix_mktime" |