changeset 96100:56850301da07

(distclean): Remove makefile.
author Eli Zaretskii <eliz@gnu.org>
date Fri, 20 Jun 2008 15:10:58 +0000
parents eb403674cfbf
children 9180cf541496
files doc/lispintro/makefile.w32-in
diffstat 1 files changed, 1 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- a/doc/lispintro/makefile.w32-in	Fri Jun 20 14:59:37 2008 +0000
+++ b/doc/lispintro/makefile.w32-in	Fri Jun 20 15:10:58 2008 +0000
@@ -64,6 +64,7 @@
 	- $(DEL) *.dvi $(infodir)/eintr*
 
 distclean: clean
+	- $(DEL) makefile
 
 maintainer-clean: distclean
 	- $(DEL) *.aux *.cps *.fns *.kys *.pgs *.vrs *.toc