From 04f500fe9759c8a64fa826c27bffc2edd9955775 Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Fri, 31 Jul 2020 22:45:45 +0100
Subject: [PATCH] signal player removal to that player

---
 src/error.rs  |  1 +
 src/global.rs | 10 ++++++++--
 2 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/error.rs b/src/error.rs
index a9d243fd..5371f56f 100644
--- a/src/error.rs
+++ b/src/error.rs
@@ -45,6 +45,7 @@ pub enum ServerFailure {
 #[derive(Error,Debug,Serialize,Copy,Clone)]
 pub enum ErrorSignaledViaUpdate {
   RenderingError,
+  PlayerRemoved,
 }
 display_as_debug!{ErrorSignaledViaUpdate}
 
diff --git a/src/global.rs b/src/global.rs
index 4a376ce4..63b5515d 100644
--- a/src/global.rs
+++ b/src/global.rs
@@ -397,8 +397,14 @@ impl InstanceGuard<'_> {
         if remove { clients_to_remove.insert(k); }
         !remove
       });
-      // xxx signal this client to abandon ?
-      self.updates.remove(oldplayer);
+      if let Some(mut updates) = self.updates.remove(oldplayer) {
+        updates. push(PreparedUpdate {
+          gen: self.c.g.gs.gen,
+          us : vec![ PreparedUpdateEntry::Error(
+            ErrorSignaledViaUpdate::PlayerRemoved
+          )],
+        });
+      }
       self.tokens_deregister_for_id(|id:PlayerId| id==oldplayer);
       self.tokens_deregister_for_id(|id| clients_to_remove.contains(&id));
       self.save_access_now().unwrap_or_else(
-- 
2.30.2