| author | wenzelm | 
| Fri, 08 Jan 2016 20:06:48 +0100 | |
| changeset 62106 | d6af554512d7 | 
| parent 56534 | 3ff16a7f0b2e | 
| child 62589 | b5783412bfed | 
| permissions | -rwxr-xr-x | 
| 53498 | 1 | #!/usr/bin/env bash | 
| 48944 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 2 | |
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 3 | set -e | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 4 | |
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 5 | FORMAT="$1" | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 6 | VARIANT="$2" | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 7 | |
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 8 | "$ISABELLE_TOOL" latex -o "$FORMAT" | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 9 | "$ISABELLE_TOOL" latex -o "$FORMAT" | 
| 
ac15a85e9282
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 10 |