+
+events.addEventListener("player-deregister", function(event) {
+ const players = document.getElementById("players");
+ const id = JSON.parse(event.data);
+ const player = document.getElementById("player-" + id.id);
+
+ players.removeChild(player);
+});
+
+events.addEventListener("capture", function(event_string) {
+ const players = document.getElementById("players");
+ const event = JSON.parse(event_string.data);
+ const player = document.getElementById("player-" + event.captee);
+
+ players.removeChild(player);
+});