mirror of
https://github.com/arduino/Arduino.git
synced 2025-03-22 13:19:48 +01:00
In the preferences dialog, the name of the preferences file is shown for advanced editing. If the filename is clicked, the folder containing the file is opened. However, this always used Base.getSettingsFolder, which is the folder where the settings file _normally_ resides. But when the --preferences-file option is used, the actual preferences file might be somewhere else. This commit makes sure to always open up the parent directory of the actual preferences file in use, instead of always the default one.