License?

the only requirement is that all the source code used to create the kernel binary must be under a GPL compatible license.

there is no reason that another binary that's produced couldn't be under a different license, but there would need to be an appropriate audit of any files that are shared between the two binaries to make sure that they are under a license compatible with both (which can include multiple licenses on a single file)