From 6bf4116066f40249a385f04fe974c7cad4ba72c0 Mon Sep 17 00:00:00 2001
From: Jim Blandy <jimb@red-bean.com>
Date: Wed, 11 Sep 1996 19:39:58 +0000
Subject: [PATCH] * Makefile.in (distclean): Don't forget to delete
 doc/Makefile.

---
 Makefile.in | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile.in b/Makefile.in
index 2e6a00e41..b80c8f534 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -112,6 +112,7 @@ distclean:
 	rm -f config.log
 	rm -f config.status
 	rm -f Makefile
+	rm -f doc/Makefile
 	for dir in ${subdirs}; do \
 		cd $$dir; \
 		${MAKE} distclean; \