tweaking the gutter line numbers a little

This commit is contained in:
Ben Fry
2022-07-31 17:07:32 -04:00
parent e432f675fe
commit 57823895ae
2 changed files with 2 additions and 1 deletions

View File

@@ -87,7 +87,7 @@ public abstract class Editor extends JFrame implements RunnerListener {
static public final int LEFT_GUTTER = Toolkit.zoom(45);
static public final int RIGHT_GUTTER = Toolkit.zoom(12);
static public final int GUTTER_MARGIN = Toolkit.zoom(3);
static public final int GUTTER_MARGIN = Toolkit.zoom(5);
protected MarkerColumn errorColumn;

View File

@@ -120,6 +120,7 @@ X contrib mgr: filter/dropdown vertical centering is too high
X should be resolved with both fonts now being installed
X two tier dialog box (defaulting back to Lucida)
X dialog box with stack trace (font is too small)
X try to tweak the line numbers in the gutter a bit
design/selector
X updated 4x4 for themes, foundation svg icon tweaks