No content changes yet, because nobody has edited anything in Crowdin so far.
However, this changes a few `\u003` to `<` (pretty sure that was an artefact of
how we manually generated the json files in #3649), and it removes all the
translations that are identical to the English version, which I guess is a good
thing (but doesn't make a difference in practice).
We write a hacky, one-off script to do that. We need this script only once, so
we don't bother polishing it much. We'll re-purpose it later in the branch to
convert the English translation set to JSON; that is an operation that we need
to do regularly in the future.
