From 2c6fc86fd3c43fd405fa1c5c5bba6745052b03dd Mon Sep 17 00:00:00 2001 From: Ben Fry Date: Sat, 11 Feb 2017 16:06:44 -0500 Subject: [PATCH] perhaps a better setting here --- app/src/processing/app/ui/Editor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index 19a9d825b..bc820c769 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -264,7 +264,7 @@ public abstract class Editor extends JFrame implements RunnerListener { textarea.setHorizontalOffset(JEditTextArea.leftHandGutter); //System.out.println(textarea.getPreferredSize()); textarea.setPreferredSize(new Dimension(textarea.getPreferredSize().width, - Toolkit.zoom(90))); + Toolkit.zoom(360))); { // Hack: add Numpad Slash as an alternative shortcut for Comment/Uncomment int modifiers = Toolkit.awtToolkit.getMenuShortcutKeyMask();