mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-28 03:17:16 +00:00
Speed up IDE startup time.
Signed-off-by: Akos Kitta <a.kitta@arduino.cc>
This commit is contained in:
@@ -9,12 +9,12 @@ import { SearchInWorkspaceWidget as TheiaSearchInWorkspaceWidget } from '@theia/
|
||||
@injectable()
|
||||
export class SearchInWorkspaceWidget extends TheiaSearchInWorkspaceWidget {
|
||||
@postConstruct()
|
||||
protected init(): void {
|
||||
protected override init(): void {
|
||||
super.init();
|
||||
this.title.iconClass = 'fa fa-arduino-search';
|
||||
}
|
||||
|
||||
protected renderGlobField(kind: 'include' | 'exclude'): React.ReactNode {
|
||||
protected override renderGlobField(kind: 'include' | 'exclude'): React.ReactNode {
|
||||
const currentValue = this.searchInWorkspaceOptions[kind];
|
||||
const value = (currentValue && currentValue.join(', ')) || '';
|
||||
return (
|
||||
|
||||
Reference in New Issue
Block a user