When exporting animation (one .obj file per animation frame), the old
Python OBJ exporter used to emit frame number with leading zeros, e.g.
"000012" which made sorting files by frame easier. The new C++ OBJ
exporter does not do that.
Fix that by reintroducing leading zeros. However, use 4 digits
("0012") since that matches 4 digits used in many other places, and
also it's very unlikely that someone would export more than several
thousand frames into OBJ. If that happens, it all works correctly
anyway, just without leading zeroes.
Fixes#116520
140f5f619d