#!/bin/bash set -e FORMAT="$1" VARIANT="$2" ISABELLE_PDFLATEX="xelatex" "$ISABELLE_TOOL" latex -o "$FORMAT" "$ISABELLE_TOOL" latex -o "$FORMAT"