#!/bin/bash

set -e

FORMAT="$1"
VARIANT="$2"

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

"$ISABELLE_TOOL" version > version.tex

"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
makeindex -o root.stu root.str
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o "$FORMAT"
mv root.pdf ../progtutorial.pdf


#"$ISABELLE_HOME/doc-src/sedindex" root
#+[ -f root.out ] && "$ISABELLE_HOME/doc-src/fixbookmarks" root.out
#+"$ISABELLE_TOOL" latex -o "$FORMAT"
#+"$ISABELLE_TOOL" latex -o "$FORMAT"
#$(ISABELLE_TOOL) document -o pdf  ProgTutorial/generated
#	makeindex -o ProgTutorial/generated/root.stu ProgTutorial/generated/root.str