doc-src/Tutorial/Makefile
changeset 6600 5a94bd71cc41
parent 5548 5cd3396802f5
child 6602 c5e32a3d7e12
equal deleted inserted replaced
6599:dc5bf3f40ad3 6600:5a94bd71cc41
     1 #  $Id$
     1 #
     2 #########################################################################
     2 # $Id$
     3 #									#
     3 #
     4 #	Makefile for the report "Isabelle/HOL. The Tutorial"		#
     4 
     5 #									#
     5 ## targets
     6 #########################################################################
     6 
       
     7 default: dvi
       
     8 dist: dvi
     7 
     9 
     8 
    10 
     9 FILES =  tutorial.tex basics.tex fp.tex appendix.tex \
    11 ## dependencies
    10 	 ../iman.sty ttbox.sty extra.sty
       
    11 
    12 
    12 tutorial.ps.gz:   $(FILES)
    13 include ../Makefile.in
    13 	isatool make
       
    14 	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
       
    15 	-rm tutorial.dvi*
       
    16 	latex tutorial
       
    17 	bibtex tutorial
       
    18 	latex tutorial
       
    19 	latex tutorial
       
    20 	../sedindex tutorial
       
    21 	latex tutorial
       
    22 	dvips tutorial.dvi -o tutorial.ps
       
    23 	gzip tutorial.ps
       
    24 
    14 
    25 dist:   $(FILES) 
    15 NAME = tutorial
    26 	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
    16 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
    27 	-rm tutorial.dvi*
    17 	../iman.sty ttbox.sty extra.sty
    28 	latex tutorial
       
    29 	latex tutorial
       
    30 	../sedindex tutorial
       
    31 	latex tutorial
       
    32 
    18 
    33 clean:
    19 dvi: $(NAME).dvi
    34 	@rm *.aux *.log *.toc *.idx
    20 
       
    21 $(NAME).dvi: $(FILES) isabelle_hol.eps
       
    22 	touch $(NAME).ind
       
    23 	$(LATEX) $(NAME)
       
    24 	$(RAIL) $(NAME)
       
    25 	$(BIBTEX) $(NAME)
       
    26 	$(LATEX) $(NAME)
       
    27 	$(LATEX) $(NAME)
       
    28 	$(SEDINDEX) $(NAME)
       
    29 	$(LATEX) $(NAME)