--- a/ajax.php	Sun Dec 02 15:27:21 2007 -0500
+++ b/ajax.php	Sun Dec 02 16:00:10 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') )
     {