printf_("%.1e", 9.96) prints "10.0e+00", should print "1.0e+01"

(migrated from eyalroz/printf#24):

When we 
```
printf_("%.3e", 9.96)
```
the rounding to 1 decimal precision digit makes the value 10.0, which should print as `1.0e+01` in exponent format. Unfortunately, library do not make sure and "re-normalize" the result of rounding, and produces `10.0e+00` instead.