| author | wenzelm | 
| Wed, 16 Jan 2013 21:49:56 +0100 | |
| changeset 50917 | 9459f59cff09 | 
| parent 48985 | 5386df44a037 | 
| child 53498 | 05313b45a5ae | 
| permissions | -rwxr-xr-x | 
| 48949 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 1 | #!/bin/bash | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 2 | |
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 3 | set -e | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 4 | |
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 5 | FORMAT="$1" | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 6 | VARIANT="$2" | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 7 | |
| 48985 | 8 | "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" | 
| 48956 | 9 |