1 #!/bin/bash

     2 

     3 set -e

     4 

     5 FORMAT="$1"

     6 VARIANT="$2"

     7 

     8 ISABELLE_PDFLATEX="xelatex"

     9 

    10 "$ISABELLE_TOOL" latex -o "$FORMAT"

    11 "$ISABELLE_TOOL" latex -o "$FORMAT"