diff options
Diffstat (limited to 'src/zenserver/frontend/html/pages/workspaces.js')
| -rw-r--r-- | src/zenserver/frontend/html/pages/workspaces.js | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/zenserver/frontend/html/pages/workspaces.js b/src/zenserver/frontend/html/pages/workspaces.js index d31fd7373..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 @@ -13,7 +14,7 @@ export class Page extends ZenPage this.set_title("workspaces"); // Workspace Service Stats - const stats_section = this.add_section("Workspace Service Stats"); + const stats_section = this._collapsible_section("Workspace Service Stats"); this._stats_grid = stats_section.tag().classify("grid").classify("stats-tiles"); const stats = await new Fetcher().resource("stats", "ws").json().catch(() => null); @@ -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 = ""; |