1
0
mirror of https://github.com/arduino/Arduino.git synced 2025-03-21 12:29:23 +01:00

Merge pull request #1234 from sgk/scrollTabMenu

Scroll the editor tab menu.
This commit is contained in:
Federico Fissore 2013-01-21 01:44:27 -08:00
commit 763ed07d77

View File

@ -22,6 +22,7 @@
*/
package processing.app;
import processing.app.tools.MenuScroller;
import static processing.app.I18n._;
import java.awt.*;
@ -238,6 +239,7 @@ public class EditorHeader extends JComponent {
} else {
menu = new JMenu();
MenuScroller.setScrollerFor(menu);
popup = menu.getPopupMenu();
add(popup);
popup.setLightWeightPopupEnabled(true);