perhaps a better setting here

This commit is contained in:
Ben Fry
2017-02-11 16:06:44 -05:00
parent eb4a33ec95
commit 2c6fc86fd3

View File

@@ -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();