diff options
| author | Olivier Laurent | 2019-11-27 22:11:33 +0100 |
|---|---|---|
| committer | Olivier Laurent | 2019-11-27 22:13:29 +0100 |
| commit | c3266d737bbda2b707ba1f2f78ecfe4e2e9f9ab8 (patch) | |
| tree | fe939e4e55a4c143bc72afde8f84ab3fbe173fc4 /Makefile | |
| parent | ac99c6aba0091d5c1ee9511508e25d399425b61b (diff) | |
remove *.vos and *.vok file in "make clean"
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 {} + |
