Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
latex output not needed because errors manifest themselves earlier
authornipkow
Mon, 24 Oct 2011 10:45:54 +0200
changeset 45259 d32872ce58ce
parent 45258 97f8806c3ed6
child 45260 48295059cef3
latex output not needed because errors manifest themselves earlier
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions 
--- 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
isabelle