diff options
Diffstat (limited to 'scripts/check-installed-headers.sh')
| -rw-r--r-- | scripts/check-installed-headers.sh | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/scripts/check-installed-headers.sh b/scripts/check-installed-headers.sh index 7ffd2b8e74..f7f55917f7 100644 --- a/scripts/check-installed-headers.sh +++ b/scripts/check-installed-headers.sh @@ -126,6 +126,13 @@ EOF fi ;; esac + ;; + + # Hurd and Mach headers are not standard anyway + (hurd.h | hurd/*.h | faultexc_server.h | \ + mach.h | mach_init.h | mach_error.h | mach-shortcuts.h | mach/* | \ + device/* | lock-intern.h | spin-lock.h | machine-sp.h) + continue;; esac echo :: "$header" |