Michael Stapelberg ecffbed45f default config: use workspace number, not just workspace ...

This is strictly better: if the configured name does not match the current name,
the correct workspace will still be used.

When creating a new workspace, the configured name is still used.

2019-07-28 08:58:39 -07:00

..

config

default config: use workspace number, not just workspace

2019-07-28 08:58:39 -07:00

config.keycodes

default config: use workspace number, not just workspace

2019-07-28 08:58:39 -07:00