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