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. *)