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

porting #100 to branch 1.5.x

This commit is contained in:
Federico Fissore 2012-12-19 16:23:07 +01:00
commit 2cfebc9cd0

View File

@ -744,9 +744,9 @@ public class Preferences {
// Fix for 0163 to properly use Unicode when writing preferences.txt
PrintWriter writer = PApplet.createWriter(preferencesFile);
Enumeration e = table.keys(); //properties.propertyNames();
while (e.hasMoreElements()) {
String key = (String) e.nextElement();
String[] keys = (String[])table.keySet().toArray(new String[0]);
Arrays.sort(keys);
for (String key: keys) {
if (key.startsWith("runtime."))
continue;
writer.println(key + "=" + ((String) table.get(key)));