diff -r 9a1a32bc2050 -r 2b60c89dc27f ajax.php
--- a/ajax.php	Sat Nov 24 01:04:30 2007 -0500
+++ b/ajax.php	Sat Nov 24 01:35:12 2007 -0500
@@ -21,6 +21,11 @@
     function dc_watch($n)    { return false; }
     function dc_start_timer($u) { return false; }
     function dc_stop_timer($m) { return false; }
+    function microtime_float()
+    {
+      list($usec, $sec) = explode(" ", microtime());
+      return ((float)$usec + (float)$sec);
+    }
     // Determine directory (special case for development servers)
     if ( strpos(__FILE__, '/repo/') && file_exists('.enanodev') )
     {