# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1322925216 18000
# Node ID a20daedfd1d0fa9c9ba43aeeeafdd3250b7a81eb
# Parent  62d6d452c2b82a49bda47ed9a3eeb12901c6033f
Avoid setting a Date's time with a non-integer value

diff -r 62d6d452c2b8 -r a20daedfd1d0 lib/js/urweb.js
--- 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