OK, I’ve made the changes in e392bb15ee7ad5315ca1816cf1f1fba48f759754. Does anything else need to be changed before we merge these changes?