/* * Init the FPU. * * This might not be strictly necessary since it will be initialised * for each process. However it does no harm. */