|
52792
|
1 |
#!/bin/bash
|
|
|
2 |
|
|
|
3 |
set -e
|
|
|
4 |
|
|
|
5 |
FORMAT="$1"
|
|
|
6 |
VARIANT="$2"
|
|
|
7 |
|
|
|
8 |
cp "$ISABELLE_HOME/src/Doc/iman.sty" .
|
|
|
9 |
cp "$ISABELLE_HOME/src/Doc/extra.sty" .
|
|
|
10 |
cp "$ISABELLE_HOME/src/Doc/isar.sty" .
|
|
|
11 |
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
|
|
|
12 |
|
|
|
13 |
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
|
|
|
14 |
|