Revert "Mike: last revertable commit"

This reverts commit d486b962878dd813015ad6d1bd1f4ec2aa241f83.