On Thu, Aug 29, 2019 at 10:58:03PM +0200, Miriam Ruiz wrote: > It's okay for me to remove it from the archive. I think it would be > the best. As you say, it seems to be dead upstream. Ack, I've just filed a removal bug. Cheers, Moritz