--- /dev/null
+#! /bin/sh
+
+set -e
+jobname=$1 opts=$2 file=$3 preamble=$4
+
+case ",$opts," in
+ *,pdf,*) tex=pdflatex ext=pdf;;
+ *) tex=latex ext=dvi;;
+esac
+
+for i in toc lot lof aux ind idx ilg bbl blg log; do
+ rm -f "$jobname".$i
+done
+
+$tex -jobname "$jobname" "\\relax $preamble \\input $file"
+case ",$opts," in *,bibtex,*) bibtex "$jobname".aux;; esac
+$tex -jobname "$jobname" "\\relax $preamble \\input $file"
+$tex -jobname "$jobname" "\\relax $preamble \\input $file"
+case ",$opts," in
+ *,index=*,*)
+ ist=$(echo "$opts" | sed 's:.*,index=\([^,]*\),.*$:\1:')
+ makeindex -s"$ist" "$jobname".idx
+ ;;
+esac
+$tex -jobname "$jobname" "\\relax $preamble \\input $file"
+
+echo timestamp >"$jobname".$ext-stamp