diff lib/js/urweb.js @ 824:be0988e46336

Use a timeout to avoid errors after unload
author Adam Chlipala <adamc@hcoop.net>
date Thu, 28 May 2009 11:45:45 -0400
parents 395a5d450cc0
children 14a6c0971d89
line wrap: on
line diff
--- a/lib/js/urweb.js	Thu May 28 10:35:25 2009 -0400
+++ b/lib/js/urweb.js	Thu May 28 11:45:45 2009 -0400
@@ -94,7 +94,7 @@
 }
 
 function servErr(s) {
-  runHandlers("Server", serverHandlers, s);
+  window.setTimeout(function () { runHandlers("Server", serverHandlers, s); }, 0);
 }
 
 
@@ -550,7 +550,8 @@
       }
       else {
         try {
-          servErr("Error querying remote server for messages: " + xhr.status);
+          if (xhr.status != 0)
+            servErr("Error querying remote server for messages: " + xhr.status);
         } catch (e) { servErr("Error querying remote server for messages"); }
       }
     }