ajax.php
changeset 232 2b60c89dc27f
parent 183 eec079676fe7
child 252 a007145a0ff6
--- 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') )
     {