When I was tech editing "Operating Systems Concepts", tenth edition, around seven years ago, I downloaded the Linux source and searched all .c and .h files for float and double. There aren't any. Linux does not require floating point support, and that's likely true of other operating systems, where performance is key. It also means that Linux can run on RISC V without floating point support (I know the basic CPU doesn't include it).