1
0
mirror of https://github.com/arduino/Arduino.git synced 2024-12-01 12:24:14 +01:00

Merge pull request #6130 from facchinm/allow_resizing_console_to_zero

Allow setting low values as minimum console size
This commit is contained in:
Martino Facchin 2017-08-01 11:47:01 +02:00 committed by GitHub
commit ad02e4940c

View File

@ -103,9 +103,8 @@ public class EditorConsole extends JScrollPane {
FontMetrics metrics = getFontMetrics(actualFont); FontMetrics metrics = getFontMetrics(actualFont);
int height = metrics.getAscent() + metrics.getDescent(); int height = metrics.getAscent() + metrics.getDescent();
int lines = PreferencesData.getInteger("console.lines"); int lines = PreferencesData.getInteger("console.lines");
int sizeFudge = 6; //10; // unclear why this is necessary, but it is setPreferredSize(new Dimension(100, (height * lines)));
setPreferredSize(new Dimension(100, (height * lines) + sizeFudge)); setMinimumSize(new Dimension(100, (height * lines)));
setMinimumSize(new Dimension(100, (height * 5) + sizeFudge));
EditorConsole.init(stdOutStyle, System.out, stdErrStyle, System.err); EditorConsole.init(stdOutStyle, System.out, stdErrStyle, System.err);
} }