1 #!/bin/bash

     2 

     3 set -e

     4 

     5 FORMAT="$1"

     6 VARIANT="$2"

     7 

     8 hg parent --template '{date|shortdate}' > tip.tex

     9 

    10 "$ISABELLE_TOOL" version > version.tex

    11 

    12 "$ISABELLE_TOOL" latex -o "$FORMAT"

    13 "$ISABELLE_TOOL" latex -o bbl

    14 makeindex -o root.stu root.str

    15 "$ISABELLE_TOOL" latex -o "$FORMAT"

    16 "$ISABELLE_TOOL" latex -o "$FORMAT"

    17 mv root.pdf ../progtutorial.pdf

    18 

    19 

    20 #"$ISABELLE_HOME/doc-src/sedindex" root

    21 #+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out

    22 #+"$ISABELLE_TOOL" latex -o "$FORMAT"

    23 #+"$ISABELLE_TOOL" latex -o "$FORMAT"

    24 #$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated

    25 #	makeindex -o ProgTutorial/generated/root.stu ProgTutorial/generated/root.str