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 ] "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 ;