| author | wenzelm | 
| Sat, 11 Apr 2015 13:12:57 +0200 | |
| changeset 60011 | 3eef7a43cd51 | 
| parent 56534 | 3ff16a7f0b2e | 
| permissions | -rwxr-xr-x | 
| 53498 | 1 | #!/usr/bin/env bash | 
| 48948 
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 | "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" | 
| 48956 | 9 |