On Thu, Aug 2, 2018 at 2:39 PM WGH <wgh@torlan.ru> wrote:>> I've just found one public report of this bug, though:> https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=900442Yeah, it does sound like we should fix this issue.Ilya? Linus