diff options
| -rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile b/Makefile index 0b66f8d92d610..28607c9b1bb69 100644 --- a/Makefile +++ b/Makefile @@ -522,8 +522,8 @@ TARGET!= uname -m .endif .if defined(MAKE_ALL_KERNELS) _THINNER=cat -.elif defined(MAKE_GENERIC_KERNELS) -_THINNER=grep "GENERIC" || true +.elif defined(MAKE_LINT_KERNELS) +_THINNER=grep 'LINT' || true .else _THINNER=xargs grep -L "^.NO_UNIVERSE" || true .endif |