Matthijs Kooijman d6333f8f37 Don't save a new preferences file in Preferences.init ... Preferences.init would write out the default preferences when no preference file previously existed. This would cause a default preferences file to be written even when --no-save-prefs was passed, due to the ordering of things. However, since the Base constructor now already calls Preferences.save(), there is no need for Preferences.init to also do this. Since Base calls this after parsing the commandline, the --no-save-prefs option is now also properly respected.		2014-08-19 09:16:47 +02:00
..
cc/arduino/packages	Better check for programmers configuration when uploading using programmer	2014-08-06 15:20:53 +02:00
processing/app	Don't save a new preferences file in Preferences.init	2014-08-19 09:16:47 +02:00