Use a timeout to avoid errors after unload

1 files changed, 3 insertions, 2 deletions

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 2b4d2643..40b170c4 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -94,7 +94,7 @@ function onServerError(f) {
 }
 
 function servErr(s) {
-  runHandlers("Server", serverHandlers, s);
+  window.setTimeout(function () { runHandlers("Server", serverHandlers, s); }, 0);
 }
 
 
@@ -550,7 +550,8 @@ function listener() {
       }
       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"); }
       }
     }