Default real numbers output precision improved.

It is now 1+13 significant digits in total, to prevent "strange" results when printing values like 0.1 and to round DBL_MAX down.
8 jobs for master in 4 minutes and 17 seconds (queued for 2 seconds)
Status Job ID Name Coverage
  Configure
passed #4749
mac
configure:mac

00:00:39

passed #4750
windows
configure:win32

00:00:26

 
  Build
passed #4752
mac
build:mac

00:02:34

passed #4751
windows
build:win32

00:01:51

 
  Dist
passed #4754
mac
dist:mac

00:00:22

passed #4753
windows
dist:win32

00:00:18

 
  Pack
passed #4756
mac
pack:mac

00:00:37

passed #4755
windows
pack:win32

00:00:28