About gnome-shell-extensions ============================ GNOME Shell Extensions is a collection of extensions providing additional and optional functionality to GNOME Shell. Most extensions can be installed by configuring --prefix=$HOME/.local, and will be picked automatically at next login.
News ==== * apps-menu: Fix height on HiDPI systems [Florian; #102] * window-list: Only switch between windows on active workspace when scrolling [Florian; #78] Contributors: Florian Müllner Download ======== https://download.gnome.org/sources/gnome-shell-extensions/3.30/gnome-shell-extensions-3.30.1.tar.xz (194K) sha256sum: b7301209ff143f9e83d43f9521ab53c9f8db0104ce562e4ec8a49c5e1cb13dbf _______________________________________________ gnome-shell-list mailing list gnome-shell-list@gnome.org https://mail.gnome.org/mailman/listinfo/gnome-shell-list
