answered 2019-11-01 17:04:43 +0000
I've pointed to this question, and noted that changing the sort might be a worthwhile improvement, on the bug in question.
