1
0
mirror of https://github.com/arduino/Arduino.git synced 2025-01-17 06:52:18 +01:00

Merge branch 'master' of github.com:arduino/Arduino

This commit is contained in:
Cristian Maglie 2015-05-26 10:47:30 +02:00
commit af512be286
2 changed files with 6 additions and 3 deletions

View File

@ -421,8 +421,11 @@ public class FindReplace extends JFrame implements ActionListener {
public void replaceAll() {
if (findField.getText().length() == 0)
return;
// move to the beginning
editor.setSelection(0, 0);
if (searchAllFiles)
editor.getSketch().setCurrentCode(0); // select the first tab
editor.setSelection(0, 0); // move to the beginning
boolean foundAtLeastOne = false;
while (true) {

View File

@ -482,7 +482,7 @@ public class MenuScroller {
double screenHeight = java.awt.Toolkit.getDefaultToolkit().getScreenSize().getHeight();
int maxItems = (int) ((screenHeight - arrowMenuItemHeight * 2 - menuBorderHeight) / itemHeight);
maxItems -= maxItems / 3;
maxItems -= maxItems / 4;
return maxItems;
}