Runtime: use puts instead of printf("%s\n")

[dra27]

Minor refactoring (split off from #9284)

[xavierleroy]

I see no good reason for this change.

Performance-wise, these uses of printf are not critical, and GCC gladly optimizes printf("%s\n", s) into puts(s) already.

Legibility-wise, I find printf("%s\n") clearer: it is obvious that a newline is printed after the string, I don't have to remember that puts(s) adds a newline but fputs(s, stdout) doesn't.

[dra27]

I generally eschew printf unless I need it (but print_endline is, of course, a better named function!). It's gone in the other PRs which caused me to switch it, too!