This commit is in reference to issue # 0015767. Originally, the clock
precision for the animation toolbar was set to 17 digits of precision. Now,
this value is definable as an Animation setting (its default is 17).