src/Doc/Tutorial/document/build
author wenzelm
Tue, 10 Sep 2013 11:57:53 +0200
changeset 54635 05313b45a5ae
parent 51441 d2c60ada3ece
child 57876 3ff16a7f0b2e
permissions -rwxr-xr-x
more portable hash-bang;
wenzelm@54635
     1
#!/usr/bin/env bash
wenzelm@49981
     2
wenzelm@49981
     3
set -e
wenzelm@49981
     4
wenzelm@49981
     5
FORMAT="$1"
wenzelm@49981
     6
VARIANT="$2"
wenzelm@49981
     7
wenzelm@50087
     8
"$ISABELLE_TOOL" logo HOL
wenzelm@49981
     9
wenzelm@50000
    10
cp "$ISABELLE_HOME/src/Doc/ttbox.sty" .
wenzelm@50000
    11
cp "$ISABELLE_HOME/src/Doc/manual.bib" .
wenzelm@49981
    12
wenzelm@50000
    13
cp "$ISABELLE_HOME/src/Doc/Tutorial/ToyList/ToyList1" .
wenzelm@50000
    14
cp "$ISABELLE_HOME/src/Doc/Tutorial/ToyList/ToyList2" .
wenzelm@49981
    15
wenzelm@49981
    16
"$ISABELLE_TOOL" latex -o sty
wenzelm@50000
    17
cp "$ISABELLE_HOME/src/Doc/pdfsetup.sty" .
wenzelm@49981
    18
wenzelm@49981
    19
"$ISABELLE_TOOL" latex -o "$FORMAT"
wenzelm@49981
    20
"$ISABELLE_TOOL" latex -o bbl
wenzelm@49986
    21
./isa-index root
wenzelm@49981
    22
"$ISABELLE_TOOL" latex -o "$FORMAT"
wenzelm@50000
    23
[ -f root.out ] && "$ISABELLE_HOME/src/Doc/fixbookmarks" root.out
wenzelm@49981
    24
"$ISABELLE_TOOL" latex -o "$FORMAT"