# HG changeset patch # User nipkow # Date 1319445954 -7200 # Node ID d32872ce58ce964ca7b93f4cd7fd875c589094ef # Parent 97f8806c3ed666a72e850cf7a8e06fd1b10848b1 latex output not needed because errors manifest themselves earlier diff -r 97f8806c3ed6 -r d32872ce58ce src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Oct 23 23:11:53 2011 +0200 +++ b/src/HOL/IsaMakefile Mon Oct 24 10:45:54 2011 +0200 @@ -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 + @cd IMP && $(ISABELLE_TOOL) usedir -g true -D generated -b $(OUT)/HOL HOL-IMP && cd generated && pdflatex root.tex > /dev/null ## HOL-IMPP