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 /dev | |
| parent | 9ecfe459660a5a1e6e59948d92bc5a9fae9e9c36 (diff) | |
| parent | 8fcbbbe80d101fdd99387b80e3a82f1dd17dfbdf (diff) | |
Merge PR #11267: FIND_SKIP_DIRS (make): ignore all dot directories
Reviewed-by: gares
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions