66 |
mc.setFont (new Font ("Dialog", Font.PLAIN, 12)); |
mc.setFont (new Font ("Dialog", Font.PLAIN, 12)); |
67 |
} |
} |
68 |
|
|
69 |
|
// FIXME: remove this method or replace it with one that does |
70 |
|
// something useful. |
71 |
/* In Gnome, help menus are no longer right flushed. */ |
/* In Gnome, help menus are no longer right flushed. */ |
72 |
|
native void nativeSetHelpMenu(MenuPeer menuPeer); |
73 |
|
|
74 |
public void addHelpMenu (Menu menu) |
public void addHelpMenu (Menu menu) |
75 |
{ |
{ |
76 |
addMenu (menu); |
// nativeSetHelpMenu((MenuPeer) menu.getPeer()); |
77 |
} |
} |
78 |
|
|
79 |
public void addMenu (Menu menu) |
public void addMenu (Menu menu) |