… and drop mere echo'ing of them to the build log.

This will make it easier to debug builds: looking at a dedicated file is easier
than finding the relevant info in a huge build log.

At this point, it doesn't feel worth it to make the generated file
machine-readable, but surely we can do it if/when we need that later on.