From bfbee488aba1546086faaaa61f7657a6a927115c Mon Sep 17 00:00:00 2001
From: Ofek Shilon <ofekshilon@gmail.com>
Date: Tue, 14 May 2024 18:39:11 +0300
Subject: [PATCH] Tree.updateTitle/getPaneName isn't recognized as used,
 because PaneRenaming is untyped

---
 static/panes/tree.ts | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/static/panes/tree.ts b/static/panes/tree.ts
index d989dec3535..14a88ab3e3d 100644
--- a/static/panes/tree.ts
+++ b/static/panes/tree.ts
@@ -76,6 +76,7 @@ export class Tree {
     private debouncedEmitChange: () => void = () => {};
     private hideable: JQuery;
     private readonly topBar: JQuery;
+    private paneName: string;
     private paneRenaming: PaneRenaming;
 
     constructor(hub: Hub, container: Container, state: TreeState) {
@@ -723,6 +724,15 @@ export class Tree {
             this.sendCompileRequests();
         }, newSettings.delayAfterChange);
     }
+    private getPaneName() {
+        return `Tree #${this.id}`;
+    }
+
+    // eslint-disable-next-line no-unused-vars
+    updateTitle() {
+        const name = this.paneName ? this.paneName : this.getPaneName();
+        this.container.setTitle(escapeHTML(name));
+    }
 
     private close() {
         this.eventHub.unsubscribe();