| author | haftmann | 
| Tue, 20 Jun 2017 13:07:47 +0200 | |
| changeset 66148 | 5e60c2d0a1f1 | 
| 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 |