Correction to my comment above: the patch at https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=809344 is preferable to the patch as proposed; thanks @philroche.
Correction to my comment above: the patch at https:/ /bugs.debian. org/cgi- bin/bugreport. cgi?bug= 809344 is preferable to the patch as proposed; thanks @philroche.