+ public static File last_logdir() {
+ synchronized (backend) {
+ if (last_logdir == null)
+ last_logdir = logdir;
+ return last_logdir;
+ }
+ }
+
+ public static void set_last_logdir(File file) {
+ synchronized(backend) {
+ if (file != null && !file.isDirectory())
+ file = file.getParentFile();
+ if (file == null)
+ file = new File(".");
+ last_logdir = file;
+ }
+ }
+