From 1d665edd5c1994bbb91454cf910511d84cfc8f5e Mon Sep 17 00:00:00 2001
From: Kimaya Bedarkar <kbedarka@mpi-sws.org>
Date: Fri, 4 Apr 2025 16:33:41 +0200
Subject: [PATCH] vacuum vok and vos files

---
 Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index 36fc9fa27..9ab0ba95f 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:
-- 
GitLab