diff -r c13e54126fcd -r 0b3ff84bab29 doc-src/System/Makefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Makefile Mon May 12 18:26:53 1997 +0200 @@ -0,0 +1,31 @@ +# $Id$ +######################################################################### +# # +# Makefile for the report "The Isabelle System Manual" # +# # +######################################################################### + + +FILES = system.tex \ + ../iman.sty ../extra.sty + +system.dvi.gz: $(FILES) + -rm system.dvi* + latex system + rail system + bibtex system + latex system + latex system + ../sedindex system + latex system + gzip -f system.dvi + +dist: $(FILES) + -rm system.dvi* + latex system + latex system + ../sedindex system + latex system + +clean: + @rm *.aux *.log *.toc *.idx