On Tue, 17 Nov 2015, Paul Wise wrote: > I use it randomly so it would be annoying if it were removed. > > I'd suggest trying to get it included in the gnome-shell-extensions > repository, that way it will get more users and maintainers.
Good idea, I submitted this: https://bugzilla.gnome.org/show_bug.cgi?id=758216 Cheers, -- Raphaël Hertzog ◈ Debian Developer Support Debian LTS: http://www.freexian.com/services/debian-lts.html Learn to master Debian: http://debian-handbook.info/get/
