| author | wenzelm | 
| Wed, 14 May 2014 12:00:18 +0200 | |
| changeset 56958 | b2c2f74d1c93 | 
| parent 56534 | 3ff16a7f0b2e | 
| child 62589 | b5783412bfed | 
| permissions | -rwxr-xr-x | 
| 53498 | 1 | #!/usr/bin/env bash | 
| 48966 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 2 | |
| 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 3 | set -e | 
| 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 4 | |
| 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 5 | FORMAT="$1" | 
| 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 6 | VARIANT="$2" | 
| 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 7 | |
| 49072 
747835eb2782
"isabelle logo" produces EPS and PDF format simultaneously;
 wenzelm parents: 
48985diff
changeset | 8 | "$ISABELLE_TOOL" logo HOL | 
| 48966 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 9 | "$ISABELLE_TOOL" latex -o "$FORMAT" | 
| 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 10 | "$ISABELLE_TOOL" latex -o bbl | 
| 48971 | 11 | ./isa-index root | 
| 48966 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 12 | "$ISABELLE_TOOL" latex -o "$FORMAT" | 
| 48985 | 13 | [ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out | 
| 48966 
6e15de7dd871
more standard document preparation within session context: avoid clashes with generated .tex files, even on case-insensible file-system;
 wenzelm parents: diff
changeset | 14 | "$ISABELLE_TOOL" latex -o "$FORMAT" |