From 51fd7c1930165ef7d534d3a4dc885e9c2f43028f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ole=20J=C3=B8rgen=20Br=C3=B8nner?= <olejorgenb@yahoo.no>
Date: Sun, 29 Oct 2017 11:39:04 +0100
Subject: [PATCH] Set workspace name utility function

Arguments ordered for convenience for now since the repl is the UI atm.
---
 utils.js | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/utils.js b/utils.js
index 69dc84f..379ccca 100644
--- a/utils.js
+++ b/utils.js
@@ -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;
+}