gnome-shell-extensions 3.8.1

[Giovanni Campagna <install-module master gnome org>]

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
====

* many improvements to window-list:
  - windows are activated by DND over them
  - window buttons now have the right size,
    even if the text is smaller or larger
    than the ideal
  - window buttons can be grouped automatically
    when the panel becomes crowded
  - added a workspace switcher menu
* added keyboard navigation to apps-menu
* small tweaks to classic-mode theme, in particular
  for menus
* translation updates (gl, ko, sr)



Download
========
http://download.gnome.org/sources/gnome-shell-extensions/3.8/gnome-shell-extensions-3.8.1.tar.xz (172K)
  sha256sum: f0c198dd7c185ddf5d20986c698882d39e28837e9fa9230eabd90eb7501c062f