python/nt_time: have a go at using 1_000_000 number separators.