Merge dev into main #23

Merged
jimmy merged 1 commits from dev into main 2026-03-06 09:21:20 +08:00
Showing only changes of commit b0f66f9650 - Show all commits
@@ -135,11 +135,12 @@
}
}
ws.onopen = () => { ws.send(token); updateTab(tabId, { connected: true }); sendSize(); };
ws.onopen = () => { ws.send(token); updateTab(tabId, { connected: true, error: "" }); sendSize(); };
ws.onmessage = (e) => term.write(new Uint8Array(e.data));
ws.onclose = () => {
updateTab(tabId, { connected: false });
term.write("\r\n\x1b[90m[Connection closed]\x1b[0m");
ws.onclose = (e) => {
const reason = e.reason || `Connection closed (code ${e.code})`;
updateTab(tabId, { connected: false, error: reason });
term.write(`\r\n\x1b[90m[${reason}]\x1b[0m`);
};
ws.onerror = () => updateTab(tabId, { connected: false, error: "Connection failed" });
term.onData((data) => ws.readyState === 1 && ws.send(new TextEncoder().encode(data)));