static File jpegify(File imageFile) {
  if (isJPEGFile(imageFile)) ret imageFile;
  loading "JPEGify" {
    BufferedImage img = loadImage2(imageFile);
    File destFile = replaceExtension(imageFile, ".jpg");
    File atticFile = newFile(javaxDataDir("JPEGified original pictures"), imageFile.getName());
    atticFile = makeFileNameUnique(atticFile);
    saveJPGVerbose(destFile, img);
    moveFileVerbose(imageFile, atticFile);
    print("Conversion done.");
    ret destFile;
  }
}