| author | nipkow | 
| Sat, 06 Jan 2018 10:08:11 +0100 | |
| changeset 67344 | 9a0bb8e2be07 | 
| parent 56420 | b266e7a86485 | 
| permissions | -rwxr-xr-x | 
| 53498 | 1 | #!/usr/bin/env bash | 
| 48949 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 2 | |
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 3 | set -e | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 4 | |
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 5 | FORMAT="$1" | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 6 | VARIANT="$2" | 
| 
a773af3e37d6
more standard document preparation within session context;
 wenzelm parents: diff
changeset | 7 | |
| 48985 | 8 | "$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT" | 
| 48956 | 9 |