1.1 --- a/common/makefiles/Main.gmk Thu Aug 15 17:14:53 2013 +0200 1.2 +++ b/common/makefiles/Main.gmk Fri Aug 16 14:43:38 2013 +0200 1.3 @@ -204,7 +204,7 @@ 1.4 # If the output directory was created by configure and now becomes empty, remove it as well. 1.5 # FIXME: tmp should not be here, fix ResetTimers instead. And remove spec.sh! 1.6 dist-clean: clean 1.7 - @($(CD) $(OUTPUT_ROOT) && $(RM) -r *spec.gmk config.* configure-arguments Makefile compare.sh spec.sh tmp) 1.8 + @($(CD) $(OUTPUT_ROOT) && $(RM) -r *spec.gmk config.* configure-arguments Makefile compare.sh spec.sh tmp javacservers) 1.9 @$(if $(filter $(CONF_NAME),$(notdir $(OUTPUT_ROOT))), \ 1.10 if test "x`$(LS) $(OUTPUT_ROOT)`" != x; then \ 1.11 $(ECHO) "Warning: Not removing non-empty configuration directory for '$(CONF_NAME)'" ;\