This is logically part of the next commit. But then, the git diff would
show the old file disappear and the new file appear with new content,
which would be hard to review, so it is split. This commit should
contain no changes in the content (hopefully), so can be skipped during
review.