tools/tools.mk
changeset 953 edd62c121892
parent 940 f0f9ba3f98f2
child 1001 c8ac48ba1411
     1.1 --- a/tools/tools.mk	Wed Oct 15 21:29:56 2008 +0000
     1.2 +++ b/tools/tools.mk	Tue Oct 21 16:13:46 2008 +0000
     1.3 @@ -28,4 +28,5 @@
     1.4  	@echo  '  updatetools        - Update the config tools'
     1.5  
     1.6  distclean::
     1.7 +	@$(ECHO) "  CLEAN tools"
     1.8  	$(SILENT)[ $(CT_TOP_DIR) = $(CT_LIB_DIR) ] || rm -rf $(CT_TOP_DIR)/tools