rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-02-26 20:54:22 +01:00
Code Issues Releases Activity

Make Recently used boards size configurable from preferences

Browse Source
This commit is contained in:
Martino Facchin 2019-03-08 11:24:51 +01:00
parent 14e59208b3
commit ddd876ca4e
2 changed files with 8 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
app/src/processing/app/Base.java
View File

@ -1549,9 +1549,13 @@ public class Base {
recentBoardsButtonGroup = new ButtonGroup(); recentBoardsButtonGroup = new ButtonGroup();
buttonGroupsMap = new HashMap<>(); buttonGroupsMap = new HashMap<>();
boolean hasRecentBoardsMenu = (PreferencesData.getInteger("editor.recent_boards.size", 4) != 0);
if (hasRecentBoardsMenu) {
JMenuItem recentLabel = new JMenuItem(tr("Recently used boards")); JMenuItem recentLabel = new JMenuItem(tr("Recently used boards"));
recentLabel.setEnabled(false); recentLabel.setEnabled(false);
boardMenu.add(recentLabel); boardMenu.add(recentLabel);
}
List<JMenu> platformMenus = new ArrayList<>(); List<JMenu> platformMenus = new ArrayList<>();

2
arduino-core/src/processing/app/BaseNoGui.java
View File

@ -937,7 +937,7 @@ public class BaseNoGui {
if (!recentlyUsedBoards.contains(targetBoard)) { if (!recentlyUsedBoards.contains(targetBoard)) {
recentlyUsedBoards.add(targetBoard); recentlyUsedBoards.add(targetBoard);
} }
if (recentlyUsedBoards.size() > 4) { if (recentlyUsedBoards.size() > PreferencesData.getInteger("editor.recent_boards.size", 4)) {
recentlyUsedBoards.remove(); recentlyUsedBoards.remove();
} }
} }