mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-14 12:49:28 +00:00
Added a workaround for Theia's auto-save issue.
Ref: eclipse-theia/theia#8722 Signed-off-by: Akos Kitta <kittaakos@typefox.io>
This commit is contained in:
@@ -0,0 +1,21 @@
|
||||
import { injectable, postConstruct } from 'inversify';
|
||||
import { EditorCommandContribution as TheiaEditorCommandContribution } from '@theia/editor/lib/browser/editor-command';
|
||||
|
||||
@injectable()
|
||||
export class EditorCommandContribution extends TheiaEditorCommandContribution {
|
||||
|
||||
@postConstruct()
|
||||
protected init(): void {
|
||||
// Workaround for https://github.com/eclipse-theia/theia/issues/8722.
|
||||
this.editorPreferences.onPreferenceChanged(({ preferenceName, newValue, oldValue }) => {
|
||||
if (preferenceName === 'editor.autoSave') {
|
||||
const autoSaveWasOnBeforeChange = !oldValue || oldValue === 'on';
|
||||
const autoSaveIsOnAfterChange = !newValue || newValue === 'on';
|
||||
if (!autoSaveWasOnBeforeChange && autoSaveIsOnAfterChange) {
|
||||
this.shell.saveAll();
|
||||
}
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
}
|
||||
Reference in New Issue
Block a user