diff --git a/Makefile b/Makefile index 148a270c64c863af35b55240902a5238f21d41e7..92f9115e4ed845c9ebf50f92d410fcb61076afff 100644 --- a/Makefile +++ b/Makefile @@ -210,10 +210,10 @@ WTESTS=dune exec --root ptests -- frama-c-wtests wtests-help: $(WTESTS) --help -# Removes all dune files generated for testing +# Removes all dune files generated for testing: xargs -n 10 avoids a too long line .PHONY: purge-tests purge-tests: - find $(PURGED_PTEST_DIRS) -name dune | grep -e "/oracle.*/dune\|/result.*/dune" | xargs --no-run-if-empty rm + find $(PURGED_PTEST_DIRS) -name dune | grep -e "/oracle.*/dune\|/result.*/dune" | xargs --no-run-if-empty -n 10 rm # Force the full cleaning of the testing environment .PHONY: clean-tests