From 9f99c76b6c8df773c28fa1d7c6d7c593cf9a6179 Mon Sep 17 00:00:00 2001 From: peter Date: Sun, 19 Feb 2012 15:13:27 +0100 Subject: [PATCH] wider gutter --- .../intellij/openapi/editor/impl/EditorGutterComponentImpl.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/platform/platform-impl/src/com/intellij/openapi/editor/impl/EditorGutterComponentImpl.java b/platform/platform-impl/src/com/intellij/openapi/editor/impl/EditorGutterComponentImpl.java index 983810f02c62..13e2528ae26a 100644 --- a/platform/platform-impl/src/com/intellij/openapi/editor/impl/EditorGutterComponentImpl.java +++ b/platform/platform-impl/src/com/intellij/openapi/editor/impl/EditorGutterComponentImpl.java @@ -72,7 +72,7 @@ import java.util.List; class EditorGutterComponentImpl extends EditorGutterComponentEx implements MouseListener, MouseMotionListener { private static final Logger LOG = Logger.getInstance("#com.intellij.openapi.editor.impl.EditorGutterComponentImpl"); private static final int START_ICON_AREA_WIDTH = 15; - private static final int FREE_PAINTERS_AREA_WIDTH = 3; + private static final int FREE_PAINTERS_AREA_WIDTH = 5; private static final int GAP_BETWEEN_ICONS = 3; private static final TooltipGroup GUTTER_TOOLTIP_GROUP = new TooltipGroup("GUTTER_TOOLTIP_GROUP", 0);