diff -r 539735ddaea9 -r 9bb2e34df0cd doc-src/Makefile.in
--- a/doc-src/Makefile.in	Wed Dec 06 11:47:21 2000 +0100
+++ b/doc-src/Makefile.in	Wed Dec 06 12:26:26 2000 +0100
@@ -13,8 +13,10 @@
 SEDINDEX = ../sedindex
 FIXBOOKMARKS = perl -pi ../fixbookmarks.pl
 
-GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.ilg *.blg *.out
-OUTPUT = *.dvi *.pdf *.ps
+DEFAULT_GARBAGE = *.aux *.log *.toc *.idx *.rai *.rao *.bbl *.ind *.ilg *.blg *.out
+DEFAULT_OUTPUT = *.dvi *.pdf *.ps
+GARBAGE =
+OUTPUT =
 
 
 ## actions
@@ -22,10 +24,10 @@
 nothing:
 
 clean:
-	@rm -f $(GARBAGE)
+	@rm -f $(DEFAULT_GARBAGE) $(GARBAGE)
 
 mrproper:
-	@rm -f $(OUTPUT) $(GARBAGE)
+	@rm -f $(DEFAULT_GARBAGE) $(DEFAULT_OUTPUT) $(GARBAGE) $(OUTPUT)
 
 
 isabelle.eps: