diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-22 13:39:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-22 13:39:43 +0200 |
| commit | 73d9e569687551a858f923e02a0a8a26801ed135 (patch) | |
| tree | 71d2b03c11e75af4dfd022e2de351cfde2266fc7 /test-suite/Makefile | |
| parent | 4bbf13bb31ac5eac24d195f67624c2ab03bb51ac (diff) | |
test suite: clean more things (glob, MExtraction.out, distclean aux)
NB: I made .aux be cleaned only with distclean imitating the main Makefile.
Diffstat (limited to 'test-suite/Makefile')
| -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 |