| changeset 3165 | 80818995eb76 |
| parent 3162 | 78fa85d44e68 |
| child 6629 | 6edc66a9d80b |
--- 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 +