Printing single-precision floating point values

[Uladzislau Paulovich]

How to use printf() function to print single-precision floating point
values on the architecture that doesn't support double-precision
floating point values? I've just found out that vfprintf() function uses
"isinf(double)" function even for printing floats and therefore it
crashes on my target architecture (armv7m-hardfloat-eabi).

Thanks,
Uladzislau.