diff options
| author | Gaëtan Gilbert | 2019-12-09 22:41:38 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-12-16 17:01:02 +0100 |
| commit | 8fcbbbe80d101fdd99387b80e3a82f1dd17dfbdf (patch) | |
| tree | 78cb74bb582291d510981242361546192494f495 /kernel/nativecode.ml | |
| parent | a9ed928ac9cf245b802c93f7952888817bc2e50c (diff) | |
FIND_SKIP_DIRS (make): ignore all dot directories
Fix #11266
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions