remove dev tools menu item (arduino#882)

kittaakos · Mar 8, 2022 · 9e89964 · 9e89964
1 parent 04c3d0c
commit 9e89964
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/arduino-ide-extension/src/browser/contributions/help.ts b/arduino-ide-extension/src/browser/contributions/help.ts
@@ -14,6 +14,7 @@ import {
 } from './contribution';
 import { nls } from '@theia/core/lib/common';
 import { IDEUpdaterCommands } from '../ide-updater/ide-updater-commands';
+import { ElectronCommands } from '@theia/core/lib/electron-browser/menu/electron-menu-contribution';
 
 @injectable()
 export class Help extends Contribution {
@@ -87,6 +88,10 @@ export class Help extends Contribution {
   }
 
   registerMenus(registry: MenuModelRegistry): void {
+    registry.unregisterMenuAction({
+      commandId: ElectronCommands.TOGGLE_DEVELOPER_TOOLS.id,
+    });
+
     registry.registerMenuAction(ArduinoMenus.HELP__MAIN_GROUP, {
       commandId: Help.Commands.GETTING_STARTED.id,
       order: '0',