| author | paulson <lp15@cam.ac.uk> | 
| Tue, 28 Apr 2015 16:23:05 +0100 | |
| changeset 60149 | 9b0825a00b1a | 
| 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 |