Ticket #1520: pref.patch

src/org/openstreetmap/josm/gui/preferences/PluginPreference.java

@@ -342 +342 @@
                 }
                 if(plugins.endsWith(","))
                         plugins = plugins.substring(0, plugins.length()-1);
-                if(plugins.length() == 0)
+                if(plugins.length() == 0) {
                         plugins = null;
-
-                String oldPlugins = Main.pref.get("plugins");
-                if (!plugins.equals(oldPlugins)) {
-                        Main.pref.put("plugins", plugins);
-                        gui.requiresRestart = true;
+                } else {
+                        String oldPlugins = Main.pref.get("plugins");
+                        if (!plugins.equals(oldPlugins)) {
+                                Main.pref.put("plugins", plugins);
+                                gui.requiresRestart = true;
+                        }
                 }
         }
 }