# HG changeset patch
# User wenzelm
# Date 1346101854 -7200
# Node ID 8cd245b8ccb17bad61cfb46caa06108acd4b6cca
# Parent  29562708e05c858cc55a91ef083e2c0465de1503
missing file;

diff -r 29562708e05c -r 8cd245b8ccb1 doc-src/Classes/document/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Classes/document/build	Mon Aug 27 23:10:54 2012 +0200
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+"$ISABELLE_TOOL" logo -o isabelle_isar.pdf Isar
+"$ISABELLE_TOOL" logo -o isabelle_isar.eps Isar
+
+cp "$ISABELLE_HOME/doc-src/iman.sty" .
+cp "$ISABELLE_HOME/doc-src/extra.sty" .
+cp "$ISABELLE_HOME/doc-src/isar.sty" .
+cp "$ISABELLE_HOME/doc-src/proof.sty" .
+cp "$ISABELLE_HOME/doc-src/manual.bib" .
+
+"$ISABELLE_TOOL" latex -o sty
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o bbl
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$ISABELLE_TOOL" latex -o "$FORMAT"
+"$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"