doc-src/System/Makefile
author wenzelm
Tue, 20 May 1997 19:29:50 +0200
changeset 3257 4e3724e0659f
parent 3172 629d63c74ddc
child 5170 33fbffd06c12
permissions -rw-r--r--
README generation;

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