Remove Makefile.boot on distclean too.

diff --git a/src/Clean.sh b/src/Clean.sh
index 2f14ccd5755274ffd6f51696fe53deeb21bd7d9a..4663da273f4755c48437a5331d974f67fcb1def0 100755 (executable)
--- a/src/Clean.sh
+++ b/src/Clean.sh
@@ -69,7 +69,12 @@ if [ ${FULL} = yes ]; then
 fi
 
 if [ ${DIST} = yes ]; then
-    maybe_rm Makefile boot-lib config.cache config.log config.status
+    maybe_rm Makefile
+    maybe_rm Makefile.boot
+    maybe_rm boot-lib           # XXX What's this?
+    maybe_rm config.cache
+    maybe_rm config.log
+    maybe_rm config.status
 fi
 
 if [ ${MAINTAINER} = yes ]; then