rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-02-26 20:54:22 +01:00
Code Issues Releases Activity

Added preferences.txt option to disable preferences save

Browse Source 
Fix #5668
This commit is contained in:
Cristian Maglie 2018-08-10 20:04:50 +02:00 committed by Cristian Maglie
parent daefdc9d7d
commit 99fe051c4a
2 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
arduino-core/src/processing/app/PreferencesData.java
View File

@ -114,6 +114,9 @@ public class PreferencesData {
if (!doSave) if (!doSave)
return; return;
if (getBoolean("preferences.readonly"))
return;
// on startup, don't worry about it // on startup, don't worry about it
// this is trying to update the prefs for who is open // this is trying to update the prefs for who is open
// before Preferences.init() has been called. // before Preferences.init() has been called.

3
build/shared/lib/preferences.txt
View File

@ -279,6 +279,9 @@ serial.line_ending=1
# default chosen language (none for none) # default chosen language (none for none)
editor.languages.current = editor.languages.current =
# Disable saving of preferences.txt file (settings will not survive Arduino IDE reboot)
preferences.readonly=false
# Debugging/Development Preferences # Debugging/Development Preferences
# --------------------------------- # ---------------------------------