mirror of
https://github.com/arduino/arduino-ide.git
synced 2025-11-05 08:28:32 +00:00
Various library/platform index update fixes
- IDE2 can start if the package index download fails. Closes #1084 - Split the lib and platform index update. Closes #1156 Signed-off-by: Akos Kitta <a.kitta@arduino.cc>
This commit is contained in:
@@ -332,6 +332,7 @@ import { OutputEditorFactory } from './theia/output/output-editor-factory';
|
||||
import { StartupTaskProvider } from '../electron-common/startup-task';
|
||||
import { DeleteSketch } from './contributions/delete-sketch';
|
||||
import { UserFields } from './contributions/user-fields';
|
||||
import { UpdateIndexes } from './contributions/update-indexes';
|
||||
|
||||
const registerArduinoThemes = () => {
|
||||
const themes: MonacoThemeJson[] = [
|
||||
@@ -744,6 +745,7 @@ export default new ContainerModule((bind, unbind, isBound, rebind) => {
|
||||
Contribution.configure(bind, CheckForUpdates);
|
||||
Contribution.configure(bind, UserFields);
|
||||
Contribution.configure(bind, DeleteSketch);
|
||||
Contribution.configure(bind, UpdateIndexes);
|
||||
|
||||
bindContributionProvider(bind, StartupTaskProvider);
|
||||
bind(StartupTaskProvider).toService(BoardsServiceProvider); // to reuse the boards config in another window
|
||||
|
||||
Reference in New Issue
Block a user