# HG changeset patch
# User wenzelm
# Date 863450669 -7200
# Node ID 80818995eb76afe6db2e13d310d534330e14fe51
# Parent  ddb0b1fdfdea3972b3d0c0c0f5696cb7bb600fcd
'dist', 'clean';

diff -r ddb0b1fdfdea -r 80818995eb76 doc-src/Inductive/Makefile
--- a/doc-src/Inductive/Makefile	Mon May 12 17:15:36 1997 +0200
+++ b/doc-src/Inductive/Makefile	Mon May 12 17:24:29 1997 +0200
@@ -10,8 +10,17 @@
 
 ind-defs.dvi.gz:   $(FILES) 
 	-rm ind-defs.dvi.gz
-	latex209 ind-defs
+	latex ind-defs
 	bibtex ind-defs
-	latex209 ind-defs
-	latex209 ind-defs
+	latex ind-defs
+	latex ind-defs
 	gzip -f ind-defs.dvi
+
+dist:   $(FILES) 
+	-rm ind-defs.dvi*
+	latex ind-defs
+	latex ind-defs
+
+clean:
+	@rm *.aux *.log *.toc
+