Set workspace name utility function

Arguments ordered for convenience for now since the repl is the UI atm.
This commit is contained in:
Ole Jørgen Brønner
2017-10-29 11:39:04 +01:00
parent f2ef36ed87
commit 51fd7c1930

View File

@@ -124,3 +124,21 @@ var toggleWindowBoxes = function(metaWindow) {
function sum(array) {
return array.reduce((a, b) => a + b, 0);
}
function setWorkspaceName(name, workspace) {
let i;
if (workspaceOrIndex === undefined) {
i = global.screen.get_active_workspace_index();
} else {
i = workspace.index();
}
let settings = new Gio.Settings({ schema_id:
'org.gnome.desktop.wm.preferences'});
let names = settings.get_strv('workspace-names');
let oldName = names[i];
names[i] = name;
settings.set_strv('workspace-names', names);
return oldName;
}