Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.Sign up
I don't understand how this came about, let alone why it might possibly result from merging #7938.
from the log you posted
For the record I can run
Also the error was not fixed by reverting #7938, so that does not make to be related to this commit.