From b7191f370687979426e56ea342afcb551a1bb5ba Mon Sep 17 00:00:00 2001
From: Eduardo Cavazos <dharmatech@finkelstein.stackeffects.info>
Date: Wed, 30 Jan 2008 01:59:46 -0600
Subject: [PATCH] ui.tools.workspace: Add workspace-dim global variable

---
 extra/ui/tools/workspace/workspace.factor | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/extra/ui/tools/workspace/workspace.factor b/extra/ui/tools/workspace/workspace.factor
index b4a6574c83..de21bf3187 100755
--- a/extra/ui/tools/workspace/workspace.factor
+++ b/extra/ui/tools/workspace/workspace.factor
@@ -69,7 +69,11 @@ M: gadget tool-scroller drop f ;
     [ find-workspace hide-popup ] <debugger>
     "Error" show-titled-popup ;
 
-M: workspace pref-dim* drop { 600 700 } ;
+SYMBOL: workspace-dim
+
+{ 600 700 } workspace-dim set-global
+
+M: workspace pref-dim* drop workspace-dim get ;
 
 M: workspace focusable-child*
     dup workspace-popup [ ] [ workspace-listener ] ?if ;