diff options
-rw-r--r-- | test-suite/Makefile | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 909cc73cd..9d84cd5c7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -117,14 +117,15 @@ run: $(SUBSYSTEMS) bugs: $(BUGS) clean: - rm -f trace .lia.cache - $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log>" + rm -f trace .lia.cache output/MExtraction.out + $(SHOW) "RM <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>" $(HIDE)find . \( \ - -name '*.vo' -o -name '*.vio' -o -name '*.log' \ + -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \ \) -print0 | xargs -0 rm -f distclean: clean - $(HIDE)find . -name '*.log' -print0 | xargs -0 rm -f + $(SHOW) "RM <**/*.aux>" + $(HIDE)find . -name '*.aux' -print0 | xargs -0 rm -f ####################################################################### # Per-subsystem targets |