#!/usr/bin/env bash

# Usage: oldpdf fileroot...

# Fileroot is the given file name or the part preceding ".tex" where
# applicable.  So you get the same behavior from "oldpdf foo" or
# "oldpdf foo.tex".

for file;
  do fileroot=${file%.*}
    echo $fileroot
    make $fileroot.dvi
    dvi2pdf $fileroot
    touch -r $fileroot.tex $fileroot.txi $fileroot.log $fileroot.dvi $fileroot.psforpdf $fileroot.pdf
done