make/Main.gmk
changeset 27329 49baf50a6840
parent 27136 ac3ebfa6b4ee
child 27595 cff167b3bfa2
child 27560 adc258b13e2c
--- a/make/Main.gmk	Fri Oct 31 11:23:03 2014 -0400
+++ b/make/Main.gmk	Wed Nov 05 09:51:33 2014 +0100
@@ -514,7 +514,7 @@
 # If the output directory was created by configure and now becomes empty, remove it as well.
 dist-clean: clean
 	($(CD) $(OUTPUT_ROOT) && $(RM) -r *spec.gmk config.* configure-arguments \
-	    Makefile compare.sh spec.sh tmp javacservers)
+	    Makefile compare.sh tmp javacservers)
 	$(if $(filter $(CONF_NAME),$(notdir $(OUTPUT_ROOT))), \
 	  if test "x`$(LS) $(OUTPUT_ROOT)`" != x; then \
 	    $(ECHO) "Warning: Not removing non-empty configuration directory for '$(CONF_NAME)'" ; \