mirror of
https://gitflic.ru/project/openide/openide.git
synced 2025-12-17 07:20:53 +07:00
Follow up to made comments in IJ-MR-156853 after it was already merged to master. Merge-request: IJ-MR-157747 Merged-by: Bartek Pacia <bartek.pacia@jetbrains.com> GitOrigin-RevId: 3b4ec6551c0d18f79eeff51954850327538fbeab