diff options
| author | coqbot-app[bot] | 2021-02-25 09:59:45 +0000 |
|---|---|---|
| committer | GitHub | 2021-02-25 09:59:45 +0000 |
| commit | 26439e3eebc3d0b76d8cf89a71cfd0de07731c26 (patch) | |
| tree | f50a123e93e990724f9c756b90d0a4660a23e433 | |
| parent | 1c80a79ae2824027edeea2439bf7e53298724be8 (diff) | |
| parent | 94d44211fa918a75482d97cc9498811fcbcda0b2 (diff) | |
Merge PR #13738: Make sure Ltac2 get cleaned too.
Reviewed-by: gares
| -rw-r--r-- | Makefile.make | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Makefile.make b/Makefile.make index 2f6781439c..eeb3e9b539 100644 --- a/Makefile.make +++ b/Makefile.make @@ -274,7 +274,7 @@ depclean: find . $(FIND_SKIP_DIRS) '(' -name '*.d' ')' -exec rm -f {} + cacheclean: - find theories test-suite -name '.*.aux' -exec rm -f {} + + find theories user-contrib test-suite -name '.*.aux' -exec rm -f {} + cleanconfig: rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist @@ -282,12 +282,12 @@ cleanconfig: distclean: clean cleanconfig cacheclean timingclean voclean: - find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ + find theories plugins user-contrib test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.glob' -o -name "*.cmxs" \ -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + - find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + + find theories plugins user-contrib test-suite -name .coq-native -empty -exec rm -rf {} + timingclean: - find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ + find theories plugins user-contrib test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ -o -name "*.v.after-timing" -o -name "*.v.timing.diff" -o -name "time-of-build.log" \ -o -name "time-of-build-before.log" -o -name "time-of-build-after.log" \ -o -name "time-of-build-pretty.log" -o -name "time-of-build-both.log" \) -exec rm -f {} + |
