karl at freefriends.org
Wed Jan 20 00:50:13 CET 2016
Currently pdftexconfig.tex sets \pdfdecimaldigits=3
In other words was there a particular reason to choose 3....
Not that I know of, but then I probably wouldn't know. (Ross, Thanh?)
However, in any case ... changing it at this late date would mean, I
think, that most PDF output from pdftex would be gratuitiously different
from what was produced before. That doesn't sound like a good outcome.
On the badness scale, I'd say that's rather worse than not being able to
share settings ... -k
More information about the tex-live