mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-02-05 16:36:56 +07:00
The previous fix incorrectly calculated height of the highlighting area and insufficiently scrolled editor up. GitOrigin-RevId: 3ce5853eb474fc4194ce4533663a183bf2814797