+ public static void set_logfile(int serial, File new_logfile) {
+ synchronized(backend) {
+ logfiles.put(serial, new_logfile);
+ backend.putString(String.format(logfilePreferenceFormat, serial), new_logfile.getPath());
+ flush_preferences();
+ }
+ }
+
+ public static File logfile(int serial) {
+ synchronized(backend) {
+ if (logfiles.containsKey(serial))
+ return logfiles.get(serial);
+ String logfile_string = backend.getString(String.format(logfilePreferenceFormat, serial), null);
+ if (logfile_string == null)
+ return null;
+ File logfile = new File(logfile_string);
+ logfiles.put(serial, logfile);
+ return logfile;
+ }
+ }
+