# HG changeset patch
# User kleing
# Date 1320276545 -39600
# Node ID 9d7b52c8eb0119c49d8c4bdf8a9dcd655d61b0b5
# Parent  2b002c6b0f7d395c6799590b95f7992011a33bb4
moved latex generation for HOL-IMP out of distribution

diff -r 2b002c6b0f7d -r 9d7b52c8eb01 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 01 10:05:28 2011 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 03 10:29:05 2011 +1100
@@ -531,7 +531,7 @@
   IMP/Sec_TypingT.thy IMP/Small_Step.thy IMP/Star.thy IMP/Types.thy \
   IMP/Util.thy IMP/VC.thy IMP/Vars.thy \
   IMP/ROOT.ML IMP/document/root.tex IMP/document/root.bib
-	@cd IMP && $(ISABELLE_TOOL) usedir -g true -D generated -b $(OUT)/HOL HOL-IMP && cd generated && pdflatex root.tex > /dev/null
+	@cd IMP && $(ISABELLE_TOOL) usedir -g true -b $(OUT)/HOL HOL-IMP
 
 ## HOL-IMPP