diff -r f0f9ba3f98f2 -r edd62c121892 tools/tools.mk
--- a/tools/tools.mk	Wed Oct 15 21:29:56 2008 +0000
+++ b/tools/tools.mk	Tue Oct 21 16:13:46 2008 +0000
@@ -28,4 +28,5 @@
 	@echo  '  updatetools        - Update the config tools'
 
 distclean::
+	@$(ECHO) "  CLEAN tools"
 	$(SILENT)[ $(CT_TOP_DIR) = $(CT_LIB_DIR) ] || rm -rf $(CT_TOP_DIR)/tools