/* * If the FPU is used inside the kernel, * kernel_fpu_end() will be defined here. */ Overall Contributors