I have found the source of the bug and provided a patch: see https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=913287
I have found the source of the bug and provided a patch: see https:/ /bugs.debian. org/cgi- bin/bugreport. cgi?bug= 913287