Uh, exactly what I had in mind. Thx. for the hint! Marko
Am 22.11.2017 um 11:25 schrieb Rui Tiago Cação Matos:
There's a fix already, see https://bugzilla.gnome.org/show_bug.cgi?id=789771 . Rui
_______________________________________________ desktop-devel-list mailing list desktop-devel-list@gnome.org https://mail.gnome.org/mailman/listinfo/desktop-devel-list
