diff options
| -rw-r--r-- | ChangeLog | 4 | ||||
| -rw-r--r-- | scripts/check-installed-headers.sh | 7 |
2 files changed, 11 insertions, 0 deletions
diff --git a/ChangeLog b/ChangeLog index 775e4c6ab3..dd65beebc6 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,7 @@ +2018-03-03 Samuel Thibault <samuel.thibault@ens-lyon.org> + + * scripts/check-installed-headers.sh: Ignore Hurd and Mach headers. + 2018-03-03 Andreas Schwab <schwab@linux-m68k.org> [BZ #22918] 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" |