mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-18 09:34:34 +07:00
Simply modify the configuration in the background and always restart the session. If the session has already ended, hide the quick fix. Merge-request: IJ-MR-194323 Merged-by: Egor Eliseev <Egor.Eliseev@jetbrains.com> (cherry picked from commit fd6c55fda3950e756d62bf508b4e274f069282c0) GitOrigin-RevId: a39a345e6ad5ae121186680585c7e22f66877807