doc-src/Inductive/Makefile
changeset 3165 80818995eb76
parent 3162 78fa85d44e68
child 6629 6edc66a9d80b
     1.1 --- a/doc-src/Inductive/Makefile	Mon May 12 17:15:36 1997 +0200
     1.2 +++ b/doc-src/Inductive/Makefile	Mon May 12 17:24:29 1997 +0200
     1.3 @@ -10,8 +10,17 @@
     1.4  
     1.5  ind-defs.dvi.gz:   $(FILES) 
     1.6  	-rm ind-defs.dvi.gz
     1.7 -	latex209 ind-defs
     1.8 +	latex ind-defs
     1.9  	bibtex ind-defs
    1.10 -	latex209 ind-defs
    1.11 -	latex209 ind-defs
    1.12 +	latex ind-defs
    1.13 +	latex ind-defs
    1.14  	gzip -f ind-defs.dvi
    1.15 +
    1.16 +dist:   $(FILES) 
    1.17 +	-rm ind-defs.dvi*
    1.18 +	latex ind-defs
    1.19 +	latex ind-defs
    1.20 +
    1.21 +clean:
    1.22 +	@rm *.aux *.log *.toc
    1.23 +