www/js/global.js

changeset 679
48f8f3fce7c0
parent 678
14322825cb3d
child 684
ccb9f24d0fe9
--- a/www/js/global.js	Thu May 14 14:38:20 2020 +0200
+++ b/www/js/global.js	Mon May 18 11:00:59 2020 +0200
@@ -751,7 +751,8 @@
 mashlist = new $.jqx.dataAdapter(mashProfileSource);
 
 /* Websocket interface. Place "websocket.onmessage = function(evt) {}" in the user script. */
-var websocket = new WebSocket('ws://'+location.hostname+'/ws');
+//var websocket = new WebSocket('ws://'+location.hostname+'/ws');
+var websocket = new ReconnectingWebSocket('ws://'+location.hostname+'/ws');
 
 websocket.onopen = function(evt) {
  console.log('WebSocket connection opened');

mercurial