Ports 6e42a417 since it's now needed, and undo an accidental deletion from d69762c4 while here (this part is not needed to fix the build, it's just in the vicinity).
