The preceding commit fixes an easy but somewhat nasty bug
that spoils graphs (REPORT=1) and the fix for it spoils
merging side branches touching these files; so it's worth
a linter procedure, even if it's pretty trivial.