| author | nipkow | 
| Thu, 12 Nov 2015 13:50:54 +0100 | |
| changeset 61645 | ae5e55d03e45 | 
| 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  |