+ # This is quite hideous -- it looks like OO.o calls the file something slightly
+ # different depending on the time format, phase of the moon or something... So
+ # we try both.
+ my $inp_ps = "output/$pdf_filename.$ext.pdf";
+ if (! -r $inp_ps) {
+ $inp_ps = "output/$pdf_filename.pdf";
+ }
+
+ system("gs $pdfopts -dCompatbilityLevel=1.4 -dNOPAUSE -dPATCH -sDEVICE=pdfwrite -dSAFER -sOutputFile=output/$pdf_filename -c '.setpdfwrite $psopts' -f - < $inp_ps >&2");