mirror of
https://github.com/arduino/Arduino.git
synced 2025-01-18 07:52:14 +01:00
bbd0128664
Before, the preferences were saved as a side effect of loading files in the Editor, but it seems better to explicitely save them as well (this should prevent problems later on, if the Editor class is no longer used in --verify or --upload mode).