changeset 5045:ef406a9b2f44

(distclean): Do delete Makefile and Makefile.in.
author Richard M. Stallman <rms@gnu.org>
date Tue, 16 Nov 1993 08:39:13 +0000
parents d3bd7baee39f
children 6edbd7807a6e
files src/Makefile.in
diffstat 1 files changed, 1 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Makefile.in	Tue Nov 16 08:24:30 1993 +0000
+++ b/src/Makefile.in	Tue Nov 16 08:39:13 1993 +0000
@@ -772,7 +772,7 @@
 /**/# This is used in making a distribution.
 /**/# Do not use it on development directories!
 distclean: clean
-	rm -f paths.h config.h ../etc/DOC-*
+	rm -f paths.h config.h Makefile Makefile.in ../etc/DOC-*
 realclean: distclean
 	rm -f TAGS
 versionclean: