1
#!/usr/bin/env bash
2
3
set -e
4
5
FORMAT="$1"
6
VARIANT="$2"
7
8
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
9