diff options
| author | Enrico Tassi | 2019-12-18 14:41:50 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-12-18 14:41:50 +0100 |
| commit | 6fb1b92c1f4a6f25f487107c3f3a89057ba2ee77 (patch) | |
| tree | f7c06862cd5125a41069be1f1d6cf050725822dc | |
| parent | 9ecfe459660a5a1e6e59948d92bc5a9fae9e9c36 (diff) | |
| parent | 8fcbbbe80d101fdd99387b80e3a82f1dd17dfbdf (diff) | |
Merge PR #11267: FIND_SKIP_DIRS (make): ignore all dot directories
Reviewed-by: gares
| -rw-r--r-- | Makefile.make | 11 |
1 files 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 |