| author | wenzelm | 
| Thu, 06 Nov 2014 13:36:19 +0100 | |
| changeset 58919 | 82a71046dce8 | 
| parent 56534 | 3ff16a7f0b2e | 
| child 62589 | b5783412bfed | 
| permissions | -rwxr-xr-x | 
| 53498 | 1  | 
#!/usr/bin/env bash  | 
| 
48947
 
7eee8b2d2099
more standard document preparation within session context;
 
wenzelm 
parents:  
diff
changeset
 | 
2  | 
|
| 
 
7eee8b2d2099
more standard document preparation within session context;
 
wenzelm 
parents:  
diff
changeset
 | 
3  | 
set -e  | 
| 
 
7eee8b2d2099
more standard document preparation within session context;
 
wenzelm 
parents:  
diff
changeset
 | 
4  | 
|
| 
 
7eee8b2d2099
more standard document preparation within session context;
 
wenzelm 
parents:  
diff
changeset
 | 
5  | 
FORMAT="$1"  | 
| 
 
7eee8b2d2099
more standard document preparation within session context;
 
wenzelm 
parents:  
diff
changeset
 | 
6  | 
VARIANT="$2"  | 
| 
 
7eee8b2d2099
more standard document preparation within session context;
 
wenzelm 
parents:  
diff
changeset
 | 
7  | 
|
| 
49072
 
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
 
wenzelm 
parents: 
48985 
diff
changeset
 | 
8  | 
"$ISABELLE_TOOL" logo HOL  | 
| 48985 | 9  | 
"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"  | 
| 48956 | 10  |