rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-01-31 20:52:13 +01:00
Code Issues Releases Activity

Allow setting low values as minimum console size

Browse Source 
Fixes #6085 when setting console.lines=0 in preferences.txt
This commit is contained in:
Martino Facchin 2017-03-27 12:52:41 +02:00
parent 647a1b0aaa
commit 0190225050
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
app/src/processing/app/EditorConsole.java
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);
} }