From ffaf409a3111df1d6d70d4c4bd791f0a890f28da Mon Sep 17 00:00:00 2001 From: Antonio Scandurra Date: Tue, 22 Mar 2022 11:06:52 +0100 Subject: [PATCH] Forget last pane's leader when such pane is removed This is just a memory optimization and doesn't cause any observable change in behavior. --- crates/workspace/src/workspace.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/crates/workspace/src/workspace.rs b/crates/workspace/src/workspace.rs index 35f3ff9a0cf6519157b16b32fb2dd49cd820df40..1f0a89a083a924d8b25791dd55da849c8e52dfaa 100644 --- a/crates/workspace/src/workspace.rs +++ b/crates/workspace/src/workspace.rs @@ -1203,6 +1203,7 @@ impl Workspace { self.panes.retain(|p| p != &pane); self.activate_pane(self.panes.last().unwrap().clone(), cx); self.unfollow(&pane, cx); + self.last_leaders_by_pane.remove(&pane.downgrade()); cx.notify(); } }