Use new Gnulib function dtoastr() to format short, accurate real numbers.