diff options
| -rw-r--r-- | otherlibs/unix/gettimeofday.c | 21 | ||||
| -rw-r--r-- | otherlibs/unix/unix.ml | 1 | ||||
| -rw-r--r-- | otherlibs/unix/unix.mli | 2 |
3 files changed, 24 insertions, 0 deletions
diff --git a/otherlibs/unix/gettimeofday.c b/otherlibs/unix/gettimeofday.c new file mode 100644 index 000000000..f67e82bdf --- /dev/null +++ b/otherlibs/unix/gettimeofday.c @@ -0,0 +1,21 @@ +#include <mlvalues.h> +#include <alloc.h> +#include "unix.h" + +#ifdef HAS_GETTIMEOFDAY + +#include <sys/types.h> +#include <sys/time.h> + +value unix_gettimeofday() /* ML */ +{ + struct timeval tp; + if (gettimeofday(&tp, NULL) == -1) uerror("gettimeofday", Nothing); + return copy_double((double) tp.tv_sec + (double) tp.tv_usec / 1e6); +} + +#else + +value unix_gettimeofday() { invalid_argument("gettimeofday not implemented"); } + +#endif diff --git a/otherlibs/unix/unix.ml b/otherlibs/unix/unix.ml index e6dcfdff0..160fb10a2 100644 --- a/otherlibs/unix/unix.ml +++ b/otherlibs/unix/unix.ml @@ -269,6 +269,7 @@ type tm = tm_isdst : bool } 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 alarm : int -> int = "unix_alarm" diff --git a/otherlibs/unix/unix.mli b/otherlibs/unix/unix.mli index 9a5f57bb9..007809f33 100644 --- a/otherlibs/unix/unix.mli +++ b/otherlibs/unix/unix.mli @@ -498,6 +498,8 @@ type tm = external time : unit -> int = "unix_time" (* Return the current time since 00:00:00 GMT, Jan. 1, 1970, in seconds. *) +external gettimeofday : unit -> float = "unix_gettimeofday" + (* Same as [time], but with resolution better than 1 second. *) external gmtime : int -> tm = "unix_gmtime" (* Convert a time in seconds, as returned by [time], into a date and a time. Assumes Greenwich meridian time zone. *) |