--- old/make/Main.gmk 2014-11-04 11:33:29.073435919 +0100 +++ new/make/Main.gmk 2014-11-04 11:33:28.949435917 +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)'" ; \