mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-04-19 13:02:30 +07:00
Before the presence of the plugins directory was used as a marker, but after IDES-6286 is implemented, it may happen that some plugins are installed for the frontend before it starts. In that case the plugins directory will be created, but we still need to migrate the plugins from the local IDE on start. So now a special file frontend-plugins-migrated.txt in the plugins directory is used as a marker. GitOrigin-RevId: 84e1f9682361256c7a30f6d78f3fa12f6dae465a