diff lib/js/urweb.js @ 1622:a20daedfd1d0

Avoid setting a Date's time with a non-integer value
author Adam Chlipala <adam@chlipala.net>
date Sat, 03 Dec 2011 10:13:36 -0500
parents 62d6d452c2b8
children f96e708b4b93
line wrap: on
line diff
--- a/lib/js/urweb.js	Sat Dec 03 10:07:50 2011 -0500
+++ b/lib/js/urweb.js	Sat Dec 03 10:13:36 2011 -0500
@@ -331,9 +331,9 @@
 function strftime(fmt, thisTime)
 {
     var thisDate = new Date();
-    thisDate.setTime(thisTime / 1000);
+    thisDate.setTime(Math.floor(thisTime / 1000));
     return Dt.format(thisDate, fmt);
-};
+}; 
 
 
 // Error handling