The JSON it produces is slightly different from what we had before:
1. indentation is a bit different;
2. it uses non-breaking space as thousands separator. I discussed this
with @lostinlight and persuaded her that NBSP is less confusing than
commas, because different cultures use different separators;
3. `lastUpdate` uses a format like "27 Jun 2023" rather than "27/06/23".
Again, I discussed this with @lostinlight and she agreed that the new
format is less confusing.
Fixes#152.