diff --git a/src/tools/GNUmakefile b/src/tools/GNUmakefile
index ba713425fe..74180f9684 100644
--- a/src/tools/GNUmakefile
+++ b/src/tools/GNUmakefile
@@ -769,7 +769,7 @@ $(STAMP_DIR):
 
 clean:
 	@test -e $(BUILDDIR)/Makefile && { cd $(BUILDDIR) && $(MAKE) clean; } || echo "Not configured"
-	rm -f build install
+	rm -rf build install
 	rm -f ../mpi_include.txt ../ga*txt
 
 realclean: