# HG changeset patch
# User Eli Zaretskii <eliz@gnu.org>
# Date 1213974658 0
# Node ID 56850301da0773e02fdb79e7772c68517b4e7e25
# Parent  eb403674cfbfde1b0e6ee3a44ac55ded266923db
(distclean): Remove makefile.

diff -r eb403674cfbf -r 56850301da07 doc/lispintro/makefile.w32-in
--- 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