doc-src/Tutorial/Makefile
author oheimb
Thu, 24 Sep 1998 15:36:16 +0200
changeset 5548 5cd3396802f5
parent 5376 60b31a24f1a6
child 6600 5a94bd71cc41
permissions -rw-r--r--
workaround for litte bug in our ln command

#  $Id$
#########################################################################
#									#
#	Makefile for the report "Isabelle/HOL. The Tutorial"		#
#									#
#########################################################################


FILES =  tutorial.tex basics.tex fp.tex appendix.tex \
	 ../iman.sty ttbox.sty extra.sty

tutorial.ps.gz:   $(FILES)
	isatool make
	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
	-rm tutorial.dvi*
	latex tutorial
	bibtex tutorial
	latex tutorial
	latex tutorial
	../sedindex tutorial
	latex tutorial
	dvips tutorial.dvi -o tutorial.ps
	gzip tutorial.ps

dist:   $(FILES) 
	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
	-rm tutorial.dvi*
	latex tutorial
	latex tutorial
	../sedindex tutorial
	latex tutorial

clean:
	@rm *.aux *.log *.toc *.idx