# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1243525545 14400
# Node ID be0988e46336d277191817a1798d3d8bfa6a8a7c
# Parent  669ac5e9a69ec3f5092555a3cf550f881835e055
Use a timeout to avoid errors after unload

diff -r 669ac5e9a69e -r be0988e46336 lib/js/urweb.js
--- 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"); }
       }
     }