diff --git a/arduino-ide-extension/src/browser/arduino-preferences.ts b/arduino-ide-extension/src/browser/arduino-preferences.ts index 5adc8b9c2..72fad503f 100644 --- a/arduino-ide-extension/src/browser/arduino-preferences.ts +++ b/arduino-ide-extension/src/browser/arduino-preferences.ts @@ -258,6 +258,12 @@ export const ArduinoConfigSchema: PreferenceSchema = { ), default: undefined, }, + 'arduino.sketch.editorOpenTimeout': { + type: 'number', + description: + 'Set the editor timeout in milliseconds to reproduce the duplicate editor tabs. See #1791', + default: 5000, + }, }, }; @@ -288,6 +294,7 @@ export interface ArduinoConfiguration { 'arduino.cli.daemon.debug': boolean; 'arduino.sketch.inoBlueprint': string; 'arduino.checkForUpdates': boolean; + 'arduino.sketch.editorOpenTimeout': number; } export const ArduinoPreferences = Symbol('ArduinoPreferences'); diff --git a/arduino-ide-extension/src/browser/contributions/open-sketch-files.ts b/arduino-ide-extension/src/browser/contributions/open-sketch-files.ts index 01fa997d3..56e877ea4 100644 --- a/arduino-ide-extension/src/browser/contributions/open-sketch-files.ts +++ b/arduino-ide-extension/src/browser/contributions/open-sketch-files.ts @@ -196,7 +196,7 @@ export class OpenSketchFiles extends SketchContribution { } }); - const timeout = 5_000; // number of ms IDE2 waits for the editor to show up in the UI + const timeout = this.preferences['arduino.sketch.editorOpenTimeout']; // number of ms IDE2 waits for the editor to show up in the UI const result: EditorWidget | undefined | 'timeout' = await Promise.race([ deferred.promise, wait(timeout).then(() => {