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