private static Vector jarFiles;  // JAR files in plugins folder with "_" in their name
private Map menuEntry2jarFile = new HashMap();
private static Vector macroFiles;  // Macros and scripts in the plugins folder
private static int userPluginsIndex; // First user plugin or submenu in Plugins menu
private static boolean addSorted;
<BUG>private static int defaultFontSize = IJ.isWindows()?14:0;
</BUG>
private static int fontSize = Prefs.getInt(Prefs.MENU_SIZE, defaultFontSize);
private static Font menuFont;
static boolean jnlp; // true when using Java WebStart

private static Vector jarFiles;  // JAR files in plugins folder with "_" in their name
private Map menuEntry2jarFile = new HashMap();
private static Vector macroFiles;  // Macros and scripts in the plugins folder
private static int userPluginsIndex; // First user plugin or submenu in Plugins menu
private static boolean addSorted;
private static int defaultFontSize = IJ.isWindows()?15:0;
private static int fontSize = Prefs.getInt(Prefs.MENU_SIZE, defaultFontSize);
private static Font menuFont;
static boolean jnlp; // true when using Java WebStart
