static long fileModificationTime(File f) {
  ret f == null ? 0 : f.lastModified();
}