2355b54f85
It's unclear why this option would be necessary, and it causes problems when people do not match it to their toolchain and CFLAGS. To set the float abi, either use a toolchain with an appropriate default or set the float-abi option in the CFLAGS environment variable. This should resolve #2586.