Re: [PATCH 2/2] makefiles: do not generate empty vmlinux.h