diff options
Diffstat (limited to 'src/zenserver/frontend/html/pages/workspaces.js')
| -rw-r--r-- | src/zenserver/frontend/html/pages/workspaces.js | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/zenserver/frontend/html/pages/workspaces.js b/src/zenserver/frontend/html/pages/workspaces.js index 2442fb35b..db02e8be1 100644 --- a/src/zenserver/frontend/html/pages/workspaces.js +++ b/src/zenserver/frontend/html/pages/workspaces.js @@ -4,6 +4,7 @@ import { ZenPage } from "./page.js" import { Fetcher } from "../util/fetcher.js" +import { copy_button } from "../util/widgets.js" //////////////////////////////////////////////////////////////////////////////// export class Page extends ZenPage @@ -157,6 +158,7 @@ export class Page extends ZenPage id_wrap.className = "ws-id-wrap"; id_wrap.appendChild(btn_expand); id_wrap.appendChild(document.createTextNode("\u00A0" + id)); + id_wrap.appendChild(copy_button(id)); const td_id = document.createElement("td"); td_id.appendChild(id_wrap); tr.appendChild(td_id); @@ -200,6 +202,7 @@ export class Page extends ZenPage _render_stats(stats) { + stats = this._merge_last_stats(stats); const grid = this._stats_grid; grid.inner().innerHTML = ""; |