print Float16 with 5 digits. fixes #5948

not a perfect fix, but better to spend an extra byte than have wrong output