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"