----- On Oct 21, 2019, at 3:12 PM, Henri Verbeet hverbeet@gmail.com wrote:
Both were attempts to address the same issue. The version that eventually made it in is commit 8e6f5ddd24158c7402b5fe28426083539eb7f617. That does look fairly different from the initial patch, so in that sense it's not unusual that someone would miss the connection between those unless they're familiar with the code in question.
Henri
Ah, that explains it.. cos i did not make that connection.
Thank you for clearing that up :)
Sveinar