--- 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