[bonzini]

Only to later add switches that chose between x87 and SSE? :)

[WalterBright]

Sadly, yes. Too bad that 80 bit floating point is essentially dead.