aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 3 insertions, 2 deletions
diff --git a/Makefile b/Makefile
index 7ba2c80f1..d1fa99ccb 100644
--- a/Makefile
+++ b/Makefile
@@ -53,8 +53,9 @@ FIND_VCS_CLAUSE:='(' \
-name 'debian' -o \
-name "$${GIT_DIR}" -o \
-name '_build' -o \
- -name '_build_ci' \
- -name 'coq-makefile' \
+ -name '_build_ci' -o \
+ -name 'coq-makefile' -o \
+ -name '.opamcache' \
')' -prune -o
define find