diff -r 5734ab5dd86d -r 31d06b5cada4 ProgTutorial/document/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/document/build	Tue Aug 28 21:23:32 2012 +0100
@@ -0,0 +1,25 @@
+#!/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 
\ No newline at end of file