Merge pull request #20 from sampottinger/fix_console_rounding

[Fork] Fix font size calculation issue in the editor console.
benfry · Nov 11, 2019 · 712a633 · 712a633
2 parents ddb8224 + 1dafe16
commit 712a633
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java
@@ -79,7 +79,10 @@ public abstract class Editor extends JFrame implements RunnerListener {
   protected EditorState state;
   protected Mode mode;
 
-  static public final int LEFT_GUTTER = Toolkit.zoom(44);
+  // There may be certain gutter sizes which cause text bounds inside the console to be calculated incorrectly. 45
+  // seems to work but change with caution.
+  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);