mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-01-05 01:50:56 +07:00
We exclude `isEmpty` until KT-72305 is fixed and it is supposed to be the default behaviour Hence, we should not ever store it to the settings or allow users to modify or remove it, because it should be transparent to the users (cherry picked from commit fbe5dc2f3aa748d780e98bb038629fe5e20b7922) IJ-CR-146866 GitOrigin-RevId: ae6f5f100f94782958c29a8d6c7ef495072fafd2