svghmi/svghmi.js
changeset 3680 20f9f0c36ad6
parent 3664 7e8db0b44e42
child 3683 bbcbb1bba9f1
--- a/svghmi/svghmi.js	Wed Nov 09 12:14:35 2022 +0100
+++ b/svghmi/svghmi.js	Tue Nov 15 09:22:50 2022 +0100
@@ -637,6 +637,13 @@
     ws = null;
     // reconect
     // TODO : add visible notification while waiting for reload
+    console.log(evt.wasClean)
+    console.log(evt.reason)
+    if(evt.code=1000){
+        // Do not attempt to reconnect immediately in case of Normal Closure
+        window.alert("Connection closed by server");
+        location.reload();
+    }
     window.setTimeout(create_ws, reconnect_delay);
     reconnect_delay += 500;
 };