Fix issue #1249
Issue #1249 (closed) was about strange characters being present in the SVG output, instead of some values. The fix was to modify gvprintdouble
using the same technique as used in xdot_fmt_num
. This prevents strange characters in the SVG output when numbers get larger.
Using a single function for formatting numbers used by all text-based output format would be ideal, but for now this solves the issue.