This problem was fixed as part of commit 5ab8b4daac1f2d314ada0fde29959264bccdeeeb on 2018-05-08. I am closing this bug, accordingly.
This problem was fixed as part of commit 5ab8b4daac1f2d3 14ada0fde299592 64bccdeeeb on 2018-05-08. I am closing this bug, accordingly.