ProgTutorial/document/build
author Christian Urban <urbanc@in.tum.de>
Thu, 04 Oct 2012 13:00:31 +0100
changeset 538 e9fd5eff62c1
parent 537 308ba2488d40
child 549 4d7543f48476
permissions -rwxr-xr-x
removed "use" for "ML_file"

#!/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 "$FORMAT"
"$ISABELLE_TOOL" latex -o bbl
makeindex -o root.stu root.str
"$ISABELLE_TOOL" latex -o "$FORMAT"
"$ISABELLE_TOOL" latex -o "$FORMAT"
cp root.pdf ../document.pdf
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