1 #!/bin/bash
2
3 ISABELLE_PDFLATEX="pdflatex"
4
3 set -e
5 set -e
6
5 FORMAT="$1"
7 FORMAT="$1"
6 VARIANT="$2"
8 VARIANT="$2"