# HG changeset patch
# User igerasim
# Date 1376657018 -7200
# Node ID f10f673d9b1798eac0955da69eab26af8b220706
# Parent  4fb877dfe5c41a441143df148c7a291a5945acd2
8023156: make dist-clean should remove javacservers directory
Reviewed-by: erikj

diff -r 4fb877dfe5c4 -r f10f673d9b17 common/makefiles/Main.gmk
--- a/common/makefiles/Main.gmk	Thu Aug 15 17:14:53 2013 +0200
+++ b/common/makefiles/Main.gmk	Fri Aug 16 14:43:38 2013 +0200
@@ -204,7 +204,7 @@
 # If the output directory was created by configure and now becomes empty, remove it as well.
 # FIXME: tmp should not be here, fix ResetTimers instead. And remove spec.sh!
 dist-clean: clean
-	@($(CD) $(OUTPUT_ROOT) && $(RM) -r *spec.gmk config.* configure-arguments Makefile compare.sh spec.sh tmp)
+	@($(CD) $(OUTPUT_ROOT) && $(RM) -r *spec.gmk config.* configure-arguments Makefile compare.sh spec.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)'" ;\