From dcc9f3eaa3a952bf75e16002918e349b4c5c05ca Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 29 Nov 2020 20:00:24 +0000
Subject: [PATCH] better handling for leave game

Signed-off-by: Ian Jackson <ijackson@chiark.greenend.org.uk>
---
 templates/script.ts | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/templates/script.ts b/templates/script.ts
index 1284ff0e..893a869d 100644
--- a/templates/script.ts
+++ b/templates/script.ts
@@ -1166,6 +1166,9 @@ function startup() {
   es.addEventListener('player-gone', function(event) {
     console.log('PLAYER-GONE', event);
     status_node.innerHTML = (event as any).data;
+    add_log_message('<strong>You are no longer in the game</strong>');
+    space.removeEventListener('mousedown', some_mousedown);
+    document.removeEventListener('keydown', some_keydown);
     es.close();
   });
   es.addEventListener('updates-expired', function(event) {
-- 
2.30.2