diff --git a/Makefile b/Makefile index 36fc9fa2768f2089f50517b86b55fa578e9baddb..9ab0ba95fa2a1d676bc987b47eed16c45d1f8b23 100644 --- a/Makefile +++ b/Makefile @@ -74,8 +74,8 @@ html gallinahtml: $(COQ_MAKEFILE) $(MAKE) -f $(COQ_MAKEFILE) $@ vacuum: allCoqProject cleanall - @echo 'VACUUMING *.vo *.glob .*.aux <empty directories>' - @find . -depth \( -iname '*.vo' -or -iname '*.glob' -or -iname '.*.aux' \) ! -path './.git/*' -delete + @echo 'VACUUMING *.vo *.vok *.vos *.glob .*.aux <empty directories>' + @find . -depth \( -iname '*.vo' -or -iname "*.vok" -or -iname "*.vok" -or -iname '*.glob' -or -iname '.*.aux' \) ! -path './.git/*' -delete @find . -depth -type d -empty ! -path './.git/*' -delete macos-clean: