Bug#823770: Fixed?

[Pietro Battiston]

Forget my previous message. This bug can just be closed, as stated by
Marc himself:
https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=822828#15