-
Christopher Subich authored
See http://stackoverflow.com/questions/16839658 -- although in most cases 16 decimal digits suffices for a double precision value, in a handful of instances 17 are necessary. At the command line, see the difference between: $ printf %.17g 1.0000000000000001 and $ printf %.16g 1.0000000000000001 Since SPINS does not provide bit-for-bit compatibility when restarting (because of the startup timestepping approach), this change is unlikely to make any significant difference to existing or future cases.
46ca2c72