1/*
2 * If the FPU is used inside the kernel,
3 * kernel_fpu_end() will be defined here.
4 */
5