mirror of
https://gitflic.ru/project/openide/openide.git
synced 2026-09-27 10:03:11 +07:00
don't use margin in ConsolePromptDecorator
IDEA-223509 GitOrigin-RevId: 7f408aa341ebf5280ca31a253c87cda1b18bced7
This commit is contained in:
committed by
intellij-monorepo-bot
parent
94d7f0dd3e
commit
2c73d4fa06
@@ -77,6 +77,8 @@ class ConsolePromptDecorator(private val myEditorEx: EditorEx) : EditorLinePaint
|
||||
|
||||
override fun gutterClosed() {}
|
||||
|
||||
override fun useMargin(): Boolean = false
|
||||
|
||||
fun update() {
|
||||
UIUtil.invokeLaterIfNeeded {
|
||||
myEditorEx.gutterComponentEx.revalidateMarkup()
|
||||
|
||||
Reference in New Issue
Block a user