From c3266d737bbda2b707ba1f2f78ecfe4e2e9f9ab8 Mon Sep 17 00:00:00 2001
From: Olivier Laurent
Date: Wed, 27 Nov 2019 22:11:33 +0100
Subject: remove *.vos and *.vok file in "make clean"

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

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 {} +
 
-- 
cgit v1.2.3