static File makeFileNameUnique_beforeExtension(File f) {
  File orig = f;
  int n = 0;
  while (f.exists())
    f = appendToFileBaseName(orig, "." + ++n);
  ret f;
}