mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
Merge remote-tracking branch 'origin/master'
This commit is contained in:
@@ -4042,7 +4042,7 @@ public final class EditorImpl extends UserDataHolderBase implements EditorEx, Hi
|
||||
|
||||
// The call below is performed because gutter's height is not updated sometimes, i.e. it sticks to the value that corresponds
|
||||
// to the situation when fold region is collapsed. That causes bottom of the gutter to not be repainted and that looks really ugly.
|
||||
getGutterComponentEx().invalidate();
|
||||
myGutterComponent.updateSize();
|
||||
}
|
||||
|
||||
// The general idea is to check if the user performed 'caret position change click' (left click most of the time) inside selection
|
||||
|
||||
Reference in New Issue
Block a user