Florian Müllner 2631f03108 windowManager: Don't remove the active workspace
Currently workspaces (except for the last one) are removed when
they become empty. While we do have special treatment for the
case where the currently active workspace is removed, we just
move directly without animations to the last workspace to avoid
ending up on a "random" workspace. However this behavior is still
a bit confusing, so keep the workspace around instead until the
user decides to move to another one.

https://bugzilla.gnome.org/show_bug.cgi?id=709064
2014-02-19 21:52:52 +01:00
..