| author | wenzelm | 
| Tue, 18 Sep 2012 19:33:45 +0200 | |
| changeset 49419 | e2726211f834 | 
| parent 48985 | 5386df44a037 | 
| child 53498 | 05313b45a5ae | 
| permissions | -rwxr-xr-x | 
| 48948 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 1 | #!/bin/bash | 
| 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 2 | |
| 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 3 | set -e | 
| 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 4 | |
| 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 5 | FORMAT="$1" | 
| 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 6 | VARIANT="$2" | 
| 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 7 | |
| 48985 | 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" . | |
| 48948 
fa49f8890ef3
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 12 | |
| 48985 | 13 | "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" | 
| 48956 | 14 |