Also fix #3499. The issue was solved by #3462.
There was a problem hiding this comment.
The reason will be displayed to describe this comment to others. Learn more.
Just a small correction if anyone is reading this: you probably meant ref #3442. Also, the previous issue is presumably solved in commit b563bcb which closed #3462.
Sorry, something went wrong.
Correct. It was my mistake and have already committed to GitHub before I noticed.