mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-05 08:28:32 +00:00
redesigned the settings menu group.
Signed-off-by: Akos Kitta <kittaakos@typefox.io>
This commit is contained in:
@@ -155,7 +155,7 @@ export class ArduinoFrontendContribution implements FrontendApplicationContribut
|
||||
this.statusBar.setElement('arduino-selected-port', {
|
||||
alignment: StatusBarAlignment.RIGHT,
|
||||
text: selectedPort ? `on ${Port.toString(selectedPort)}` : '[not connected]',
|
||||
className: 'arduino-selected-port'
|
||||
className: 'arduino-selected-port'
|
||||
});
|
||||
}
|
||||
}
|
||||
@@ -256,9 +256,6 @@ export class ArduinoFrontendContribution implements FrontendApplicationContribut
|
||||
commandId: ArduinoCommands.TOGGLE_ADVANCED_MODE.id,
|
||||
label: 'Advanced Mode'
|
||||
});
|
||||
registry.registerMenuAction([...CommonMenus.FILE_SETTINGS_SUBMENU, '3_settings_cli'], {
|
||||
commandId: ArduinoCommands.OPEN_CLI_CONFIG.id
|
||||
});
|
||||
}
|
||||
|
||||
registerKeybindings(keybindings: KeybindingRegistry): void {
|
||||
|
||||
Reference in New Issue
Block a user