diff --git a/arduino-ide-extension/src/node/tool-output-service-impl.ts b/arduino-ide-extension/src/node/tool-output-service-impl.ts index 9aca7dd4..ca9bc428 100644 --- a/arduino-ide-extension/src/node/tool-output-service-impl.ts +++ b/arduino-ide-extension/src/node/tool-output-service-impl.ts @@ -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 {