diff -r 14322825cb3d -r 48f8f3fce7c0 www/js/global.js
--- 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');