- // Only add the extension if it is not already the extension of
- // fullname.
- if (getExtension(fullname.absFileName()) != ext)
- fullname = FileName(addExtension(fullname.absFileName(), ext));
- if (fullname.isReadableFile() || mode == may_not_exist)
- return fullname;
+ int n = 0;
+ string ext = token(exts, ',', n);
+ while (!ext.empty()) {
+ // Only add the extension if it is not already the extension of
+ // fullname.
+ bool addext = getExtension(fullname.absFileName()) != ext;
+ if (addext) {
+ if (mode == check_hidpi) {
+ FileName fullname2x = FileName(addExtension(fullname.absFileName() + "@2x", ext));
+ if (fullname2x.isReadableFile())
+ return fullname2x;
+ }
+ fullname = FileName(addExtension(fullname.absFileName(), ext));
+ }
+ if (fullname.isReadableFile() || mode == may_not_exist)
+ return fullname;
+ if (addext)
+ fullname.changeExtension("");
+ ext = token(exts, ',', ++n);
+ }