doc-src/Intro/Makefile
author wenzelm
Thu Feb 20 14:59:02 1997 +0100 (1997-02-20)
changeset 2656 71097a167f0b
parent 1053 a19fbe807f91
child 2663 3ca200d880f4
permissions -rw-r--r--
made a bit more robust;
     1 #  $Id$
     2 #########################################################################
     3 #									#
     4 #	Makefile for the report "Introduction to Isabelle"		#
     5 #									#
     6 #########################################################################
     7 
     8 
     9 FILES =  intro.tex foundations.tex getting.tex advanced.tex \
    10 	 ../proof209.sty ../iman.sty ../extra.sty
    11 
    12 intro.dvi:   $(FILES) 
    13 	-rm intro.dvi*
    14 	latex209 intro
    15 	-test -f string.bib && bibtex intro
    16 	latex209 intro
    17 	latex209 intro
    18 	../sedindex intro
    19 	latex209 intro
    20 
    21 intro.dvi.gz: intro.dvi
    22 	gzip -f intro.dvi