This problem was eventually fixed in other ways, mainly by #6740 (commit 
e948df8c7ba8174337437b47dd2de2c14e98e19f).