Revert commit f86c3e7bbd88d755bc8ab0f467b486bf475656a1

This was pushed accidentally as part of an earlier branch, updating
files with a slightly different version of tools than what has been
used before.