aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorJim Fehrle2018-09-18 09:56:53 -0700
committerJim Fehrle2018-09-20 11:31:24 -0700
commit7dcc01273a18afc2921c567574c76b411c1b63d9 (patch)
treeff099b68efc57765a6b806cbc19fade31809a4fe /Makefile
parent15649c16bc4e20ef2c2b1b0ac645f83ee03c3589 (diff)
Use "rm -rf" so .coq-native directories are removed. Fixes #8496.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index d367424da6..2e4f46272e 100644
--- a/Makefile
+++ b/Makefile
@@ -268,7 +268,7 @@ distclean: clean cleanconfig cacheclean timingclean
voclean:
find theories plugins test-suite \( -name '*.vo' -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 -f {} +
+ find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} +
timingclean:
find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \