Florian Müllner bdf6af3ee3 window-list: Update workspace names in-place ...

There's no good reason to rebuild the entire menu on workspace names
changes, we can simply update the labels in-place.

https://gitlab.gnome.org/GNOME/gnome-shell-extensions/merge_requests/70

2019-07-19 13:11:09 +02:00

..

classic.css

classic: Update window-list styling

2019-07-16 11:17:11 +02:00

extension.js

window-list: Split out workspaceIndicator

2019-07-19 13:11:09 +02:00

meson.build

window-list: Split out workspaceIndicator

2019-07-19 13:11:09 +02:00

metadata.json.in

meta: Update description note for reporting bugs

2017-12-01 21:04:02 +01:00

org.gnome.shell.extensions.window-list.gschema.xml

Use Unicode in translatable strings

2017-02-16 02:20:03 +01:00

prefs.js

style: Use single-quotes for translated strings

2019-02-28 23:29:31 +01:00

stylesheet.css

window-list: Add window picker button

2019-06-28 23:02:58 +02:00

windowPicker.js

window-list: Handle closing window picker with Escape

2019-07-02 21:20:01 +02:00

workspaceIndicator.js

window-list: Update workspace names in-place

2019-07-19 13:11:09 +02:00