diff options
Diffstat (limited to 'src/webui_live.js')
| -rw-r--r-- | src/webui_live.js | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/webui_live.js b/src/webui_live.js index 12b5fef..b28fa52 100644 --- a/src/webui_live.js +++ b/src/webui_live.js @@ -2,8 +2,13 @@ const ws = new WebSocket("/webui_ws") ws.onopen = () => console.log("ws open"); -ws.onclose = () => console.warn("ws close"); ws.onerror = () => console.warn("ws error"); +ws.onclose = () => { + console.warn("ws close"); + document.body.innerHTML += + `<p style="position:absolute;top:10px;left:10px;font-size:larger;background-color:red;padding:1em;">Websocket connection lost.</p>` + setTimeout(() => globalThis.location.reload(), 500) +} ws.onmessage = ev => { const u = JSON.parse(ev.data) if (u.t == "update_worker") { |