mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-07-24 11:46:32 +00:00
dispose the tool ouput when the window closes.
Signed-off-by: Akos Kitta <kittaakos@typefox.io>
This commit is contained in:
parent
84016f4e1e
commit
a54c860dbb
@ -22,7 +22,12 @@ export class ToolOutputServiceServerImpl implements ToolOutputServiceServer {
|
||||
}
|
||||
|
||||
disposeClient(client: ToolOutputServiceClient): void {
|
||||
|
||||
const index = this.clients.indexOf(client);
|
||||
if (index === -1) {
|
||||
console.warn(`Could not dispose tools output client. It was not registered.`);
|
||||
return;
|
||||
}
|
||||
this.clients.splice(index, 1);
|
||||
}
|
||||
|
||||
dispose(): void {
|
||||
|
Loading…
x
Reference in New Issue
Block a user