From 8fcbbbe80d101fdd99387b80e3a82f1dd17dfbdf Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 9 Dec 2019 22:41:38 +0100
Subject: FIND_SKIP_DIRS (make): ignore all dot directories

Fix #11266
---
 Makefile.make | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/Makefile.make b/Makefile.make
index d8e229e4db..e19053462d 100644
--- a/Makefile.make
+++ b/Makefile.make
@@ -46,23 +46,20 @@
 
 # !! Before using FIND_SKIP_DIRS, please read how you should in the !!
 # !! FIND_SKIP_DIRS section of dev/doc/build-system.dev.txt         !!
-FIND_SKIP_DIRS:='(' \
+# "-not -name ." to avoid skipping everything since we "find ."
+# "-type d" to be able to find .merlin.in files
+FIND_SKIP_DIRS:=-not -name . '(' \
   -name '{arch}' -o \
-  -name '.svn' -o \
+  -name '.*' -type d -o \
   -name '_darcs' -o \
-  -name '.git' -o \
-  -name '.bzr' -o \
   -name 'debian' -o \
   -name "$${GIT_DIR}" -o \
   -name '_build' -o \
   -name '_build_ci' -o \
-  -name '_build_boot' -o \
   -name '_install_ci' -o \
   -name 'gramlib' -o \
   -name 'user-contrib' -o \
   -name 'test-suite' -o \
-  -name '.opamcache' -o \
-  -name '.coq-native' -o \
   -name 'plugin_tutorial' \
 ')' -prune -o
 
-- 
cgit v1.2.3