aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorOlivier Laurent2019-11-27 22:11:33 +0100
committerOlivier Laurent2019-11-27 22:13:29 +0100
commitc3266d737bbda2b707ba1f2f78ecfe4e2e9f9ab8 (patch)
treefe939e4e55a4c143bc72afde8f84ab3fbe173fc4
parentac99c6aba0091d5c1ee9511508e25d399425b61b (diff)
remove *.vos and *.vok file in "make clean"
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index d9fd03ac5a..c7d162bc56 100644
--- a/Makefile
+++ b/Makefile
@@ -284,7 +284,7 @@ cleanconfig:
distclean: clean cleanconfig cacheclean timingclean
voclean:
- find theories plugins test-suite \( -name '*.vo' -o -name '*.vio' -o -name '*.glob' -o -name "*.cmxs" \
+ find theories plugins 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 {} +