+ string result = s;
+ if (what != PATHS && contains(result, "$$pngOrjpg")) {
+ // This is for raster images and pdflatex:
+ // Since pdflatex supports both jpg and png, we choose the best format:
+ // jpg if the original file is jpg to retain the compression, else png.
+ string format = formats.getFormatFromFile(params.filename);
+ if (format == "jpg")
+ result = subst(result, "$$pngOrjpg", "jpg");
+ else
+ result = subst(result, "$$pngOrjpg", "png");
+ }
+
+ if (what == FORMATS)
+ return result;
+