static File addDateWithMillisecondsToFileName(File f) {
  ret appendToFileNameBeforeExtension(f, "." + simpleDateFormat_local("yyyyMMdd-HHmmss-SSSS").format(now()));
}