jeans/arduino-ide
1
0
Fork 0
mirror of https://github.com/arduino/arduino-ide.git synced 2025-11-05 08:28:32 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix duplicated editor tabs (#1012)

Browse Source
This commit is contained in:
Mark Sujew
2022-05-31 11:33:07 +02:00
committed by GitHub
parent 522a5c6e01
commit 5fc30bd33e
3 changed files with 18 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
arduino-ide-extension/src/browser/arduino-ide-frontend-module.ts
View File

@@ -275,6 +275,8 @@ import {
IDEUpdaterDialogWidget,
} from './dialogs/ide-updater/ide-updater-dialog';
import { ElectronIpcConnectionProvider } from '@theia/core/lib/electron-browser/messaging/electron-ipc-connection-provider';
import { EditorManager as TheiaEditorManager } from '@theia/editor/lib/browser/editor-manager';
import { EditorManager } from './theia/editor/editor-manager';
const ElementQueries = require('css-element-queries/src/ElementQueries');
@@ -507,6 +509,8 @@ export default new ContainerModule((bind, unbind, isBound, rebind) => {
bind(SearchInWorkspaceWidget).toSelf();
rebind(TheiaSearchInWorkspaceWidget).toService(SearchInWorkspaceWidget);
rebind(TheiaEditorManager).to(EditorManager);
// replace search icon
rebind(TheiaSearchInWorkspaceFactory)