--- a/www/js/global.js	Wed May 20 21:49:09 2020 +0200
+++ b/www/js/global.js	Thu May 21 14:27:56 2020 +0200
@@ -769,12 +769,6 @@
  $('#wsstatus').html('WebSocket error: ' + event.data);
 }
 
-/* Handle global menu manipulation called by the user script. */
-function ws_global(msg) {
- console.log('ws_global(' + msg + ')');
-}
-
-
 $(document).ready(function() {
 
  $('#jqxMenu').jqxMenu({